Termination proof of /tmp/tmp4st1kV/CountMetaListRec.jar

Termination of the given JBC could be proven:

0 JBC

↳1 JBCToGraph (⇒, 1090 ms)

↳2 JBCTerminationGraph

↳3 TerminationGraphToSCCProof (⇒, 0 ms)

↳4 AND

    ↳5 JBCTerminationSCC

        ↳6 SCCToIDPv1Proof (⇒, 780 ms)

        ↳7 IDP

        ↳8 IDPtoQDPProof (⇒, 0 ms)

        ↳9 QDP

        ↳10 UsableRulesProof (⇔, 0 ms)

        ↳11 QDP

        ↳12 QReductionProof (⇔, 0 ms)

        ↳13 QDP

        ↳14 UsableRulesReductionPairsProof (⇔, 0 ms)

        ↳15 QDP

        ↳16 MRRProof (⇔, 0 ms)

        ↳17 QDP

        ↳18 PisEmptyProof (⇔, 0 ms)

        ↳19 YES

    ↳20 JBCTerminationSCC

        ↳21 SCCToIDPv1Proof (⇒, 420 ms)

        ↳22 IDP

        ↳23 IDPNonInfProof (⇒, 910 ms)

        ↳24 IDP

        ↳25 IDependencyGraphProof (⇔, 0 ms)

        ↳26 IDP

        ↳27 IDPNonInfProof (⇒, 130 ms)

        ↳28 IDP

        ↳29 IDependencyGraphProof (⇔, 0 ms)

        ↳30 TRUE

(0) Obligation:

JBC Problem based on JBC Program:
Manifest-Version: 1.0 Created-By: 1.6.0_22 (Sun Microsystems Inc.) Main-Class: CountMetaListRec

public class CountMetaListRec {
	public static void main(String[] args) {
		Random.args = args;
		List l = createMetaList();

		int count = countMetaList(l);
	}

	public static int countMetaList(List cur) {
		if (cur == null) {
			return 0;
		} else {
			if (cur.value instanceof List) {
				List inner = (List) cur.value;
				cur.value = inner.next;
				cur = new List(inner.value, cur);
			}
			return 1 + countMetaList(cur.next);
		}
	}

	public static List createMetaList() {
		int count = Random.random();
		List cur = null;
		for (int i = 0; i < count; i++) {
			int innerCount = Random.random();
			List innerList = null;
			for (int j = innerCount; j > 0; j--) {
				innerList = new List(null, innerList);
			}
			cur = new List(innerList, cur);
		}

		return cur;
	}
}

class List {
	Object value;
	List next;

	public List(Object v, List n) {
		this.value = v;
		this.next = n;
	}
}


public class Random {
  static String[] args;
  static int index = 0;

  public static int random() {
    String string = args[index];
    index++;
    return string.length();
  }
}

(1) JBCToGraph (SOUND transformation)

Constructed TerminationGraph.

(2) Obligation:

Termination Graph based on JBC Program:
CountMetaListRec.main([Ljava/lang/String;)V: Graph of 66 nodes with 0 SCCs.

CountMetaListRec.createMetaList()LList;: Graph of 195 nodes with 1 SCC.

CountMetaListRec.countMetaList(LList;)I: Graph of 88 nodes with 0 SCCs.

(3) TerminationGraphToSCCProof (SOUND transformation)

Splitted TerminationGraph to 2 SCCss.

(4) Complex Obligation (AND)

(5) Obligation:

SCC of termination graph based on JBC Program.
SCC contains nodes from the following methods: CountMetaListRec.countMetaList(LList;)I
SCC calls the following helper methods: CountMetaListRec.countMetaList(LList;)I
Performed SCC analyses: UsedFieldsAnalysis

(6) SCCToIDPv1Proof (SOUND transformation)

Transformed FIGraph SCCs to IDPs. Log:

Generated 59 rules for P and 33 rules for R.

P rules:
1626_0_countMetaList_NONNULL(EOS(STATIC_1626), java.lang.Object(o1484sub), java.lang.Object(o1484sub)) → 1631_0_countMetaList_NONNULL(EOS(STATIC_1631), java.lang.Object(o1484sub), java.lang.Object(o1484sub))
1631_0_countMetaList_NONNULL(EOS(STATIC_1631), java.lang.Object(o1484sub), java.lang.Object(o1484sub)) → 1636_0_countMetaList_Load(EOS(STATIC_1636), java.lang.Object(o1484sub))
1636_0_countMetaList_Load(EOS(STATIC_1636), java.lang.Object(o1484sub)) → 1644_0_countMetaList_FieldAccess(EOS(STATIC_1644), java.lang.Object(o1484sub), java.lang.Object(o1484sub))
1644_0_countMetaList_FieldAccess(EOS(STATIC_1644), java.lang.Object(List(EOC, o1495, o1496)), java.lang.Object(List(EOC, o1495, o1496))) → 1650_0_countMetaList_FieldAccess(EOS(STATIC_1650), java.lang.Object(List(EOC, o1495, o1496)), java.lang.Object(List(EOC, o1495, o1496)))
1650_0_countMetaList_FieldAccess(EOS(STATIC_1650), java.lang.Object(List(EOC, o1495, o1496)), java.lang.Object(List(EOC, o1495, o1496))) → 1655_0_countMetaList_CheckCast(EOS(STATIC_1655), java.lang.Object(List(EOC, o1495, o1496)), o1495)
1655_0_countMetaList_CheckCast(EOS(STATIC_1655), java.lang.Object(List(EOC, java.lang.Object(o1510sub), o1496)), java.lang.Object(o1510sub)) → 1665_0_countMetaList_CheckCast(EOS(STATIC_1665), java.lang.Object(List(EOC, java.lang.Object(o1510sub), o1496)), java.lang.Object(o1510sub))
1655_0_countMetaList_CheckCast(EOS(STATIC_1655), java.lang.Object(List(EOC, NULL, o1496)), NULL) → 1666_0_countMetaList_CheckCast(EOS(STATIC_1666), java.lang.Object(List(EOC, NULL, o1496)), NULL)
1665_0_countMetaList_CheckCast(EOS(STATIC_1665), java.lang.Object(List(EOC, java.lang.Object(o1512sub), o1496)), java.lang.Object(o1512sub)) → 1677_0_countMetaList_CheckCast(EOS(STATIC_1677), java.lang.Object(List(EOC, java.lang.Object(o1512sub), o1496)), java.lang.Object(o1512sub))
1665_0_countMetaList_CheckCast(EOS(STATIC_1665), java.lang.Object(List(EOC, java.lang.Object(o1513sub), o1496)), java.lang.Object(o1513sub)) → 1678_0_countMetaList_CheckCast(EOS(STATIC_1678), java.lang.Object(List(EOC, java.lang.Object(o1513sub), o1496)), java.lang.Object(o1513sub))
1677_0_countMetaList_CheckCast(EOS(STATIC_1677), java.lang.Object(List(EOC, java.lang.Object(o1512sub), o1496)), java.lang.Object(o1512sub)) → 1684_0_countMetaList_EQ(EOS(STATIC_1684), java.lang.Object(List(EOC, java.lang.Object(o1512sub), o1496)), 1)
1684_0_countMetaList_EQ(EOS(STATIC_1684), java.lang.Object(List(EOC, java.lang.Object(o1512sub), o1496)), matching1) → 1700_0_countMetaList_Load(EOS(STATIC_1700), java.lang.Object(List(EOC, java.lang.Object(o1512sub), o1496))) | &&(>(1, 0), =(matching1, 1))
1700_0_countMetaList_Load(EOS(STATIC_1700), java.lang.Object(List(EOC, java.lang.Object(o1512sub), o1496))) → 1710_0_countMetaList_FieldAccess(EOS(STATIC_1710), java.lang.Object(List(EOC, java.lang.Object(o1512sub), o1496)), java.lang.Object(List(EOC, java.lang.Object(o1512sub), o1496)))
1710_0_countMetaList_FieldAccess(EOS(STATIC_1710), java.lang.Object(List(EOC, java.lang.Object(o1512sub), o1496)), java.lang.Object(List(EOC, java.lang.Object(o1512sub), o1496))) → 1718_0_countMetaList_CheckCast(EOS(STATIC_1718), java.lang.Object(List(EOC, java.lang.Object(o1512sub), o1496)), java.lang.Object(o1512sub))
1718_0_countMetaList_CheckCast(EOS(STATIC_1718), java.lang.Object(List(EOC, java.lang.Object(o1512sub), o1496)), java.lang.Object(o1512sub)) → 1727_0_countMetaList_Store(EOS(STATIC_1727), java.lang.Object(List(EOC, java.lang.Object(o1512sub), o1496)), java.lang.Object(o1512sub))
1727_0_countMetaList_Store(EOS(STATIC_1727), java.lang.Object(List(EOC, java.lang.Object(o1512sub), o1496)), java.lang.Object(o1512sub)) → 1737_0_countMetaList_Load(EOS(STATIC_1737), java.lang.Object(List(EOC, java.lang.Object(o1512sub), o1496)), java.lang.Object(o1512sub))
1737_0_countMetaList_Load(EOS(STATIC_1737), java.lang.Object(List(EOC, java.lang.Object(o1512sub), o1496)), java.lang.Object(o1512sub)) → 1745_0_countMetaList_Load(EOS(STATIC_1745), java.lang.Object(List(EOC, java.lang.Object(o1512sub), o1496)), java.lang.Object(o1512sub), java.lang.Object(List(EOC, java.lang.Object(o1512sub), o1496)))
1745_0_countMetaList_Load(EOS(STATIC_1745), java.lang.Object(List(EOC, java.lang.Object(o1512sub), o1496)), java.lang.Object(o1512sub), java.lang.Object(List(EOC, java.lang.Object(o1512sub), o1496))) → 1754_0_countMetaList_FieldAccess(EOS(STATIC_1754), java.lang.Object(List(EOC, java.lang.Object(o1512sub), o1496)), java.lang.Object(o1512sub), java.lang.Object(List(EOC, java.lang.Object(o1512sub), o1496)), java.lang.Object(o1512sub))
1754_0_countMetaList_FieldAccess(EOS(STATIC_1754), java.lang.Object(List(EOC, java.lang.Object(List(EOC, o1576, o1577)), o1496)), java.lang.Object(List(EOC, o1576, o1577)), java.lang.Object(List(EOC, java.lang.Object(List(EOC, o1576, o1577)), o1496)), java.lang.Object(List(EOC, o1576, o1577))) → 1765_0_countMetaList_FieldAccess(EOS(STATIC_1765), java.lang.Object(List(EOC, java.lang.Object(List(EOC, o1576, o1577)), o1496)), java.lang.Object(List(EOC, o1576, o1577)), java.lang.Object(List(EOC, java.lang.Object(List(EOC, o1576, o1577)), o1496)), java.lang.Object(List(EOC, o1576, o1577)))
1765_0_countMetaList_FieldAccess(EOS(STATIC_1765), java.lang.Object(List(EOC, java.lang.Object(List(EOC, o1576, o1577)), o1496)), java.lang.Object(List(EOC, o1576, o1577)), java.lang.Object(List(EOC, java.lang.Object(List(EOC, o1576, o1577)), o1496)), java.lang.Object(List(EOC, o1576, o1577))) → 1776_0_countMetaList_FieldAccess(EOS(STATIC_1776), java.lang.Object(List(EOC, java.lang.Object(List(EOC, o1576, o1577)), o1496)), java.lang.Object(List(EOC, o1576, o1577)), java.lang.Object(List(EOC, java.lang.Object(List(EOC, o1576, o1577)), o1496)), o1577)
1776_0_countMetaList_FieldAccess(EOS(STATIC_1776), java.lang.Object(List(EOC, java.lang.Object(List(EOC, o1576, o1577)), o1496)), java.lang.Object(List(EOC, o1576, o1577)), java.lang.Object(List(EOC, java.lang.Object(List(EOC, o1576, o1577)), o1496)), o1577) → 1789_0_countMetaList_New(EOS(STATIC_1789), java.lang.Object(List(EOC, o1577, o1496)), java.lang.Object(List(EOC, o1576, o1577)))
1789_0_countMetaList_New(EOS(STATIC_1789), java.lang.Object(List(EOC, o1577, o1496)), java.lang.Object(List(EOC, o1576, o1577))) → 1802_0_countMetaList_Duplicate(EOS(STATIC_1802), java.lang.Object(List(EOC, o1577, o1496)), java.lang.Object(List(EOC, o1576, o1577)), java.lang.Object(List(EOC, NULL, NULL)))
1802_0_countMetaList_Duplicate(EOS(STATIC_1802), java.lang.Object(List(EOC, o1577, o1496)), java.lang.Object(List(EOC, o1576, o1577)), java.lang.Object(List(EOC, NULL, NULL))) → 1813_0_countMetaList_Load(EOS(STATIC_1813), java.lang.Object(List(EOC, o1577, o1496)), java.lang.Object(List(EOC, o1576, o1577)), java.lang.Object(List(EOC, NULL, NULL)), java.lang.Object(List(EOC, NULL, NULL)))
1813_0_countMetaList_Load(EOS(STATIC_1813), java.lang.Object(List(EOC, o1577, o1496)), java.lang.Object(List(EOC, o1576, o1577)), java.lang.Object(List(EOC, NULL, NULL)), java.lang.Object(List(EOC, NULL, NULL))) → 1831_0_countMetaList_FieldAccess(EOS(STATIC_1831), java.lang.Object(List(EOC, o1577, o1496)), java.lang.Object(List(EOC, NULL, NULL)), java.lang.Object(List(EOC, NULL, NULL)), java.lang.Object(List(EOC, o1576, o1577)))
1831_0_countMetaList_FieldAccess(EOS(STATIC_1831), java.lang.Object(List(EOC, o1577, o1496)), java.lang.Object(List(EOC, NULL, NULL)), java.lang.Object(List(EOC, NULL, NULL)), java.lang.Object(List(EOC, o1576, o1577))) → 1849_0_countMetaList_Load(EOS(STATIC_1849), java.lang.Object(List(EOC, o1577, o1496)), java.lang.Object(List(EOC, NULL, NULL)), java.lang.Object(List(EOC, NULL, NULL)), o1576)
1849_0_countMetaList_Load(EOS(STATIC_1849), java.lang.Object(List(EOC, o1577, o1496)), java.lang.Object(List(EOC, NULL, NULL)), java.lang.Object(List(EOC, NULL, NULL)), o1576) → 1872_0_countMetaList_InvokeMethod(EOS(STATIC_1872), java.lang.Object(List(EOC, NULL, NULL)), java.lang.Object(List(EOC, NULL, NULL)), o1576, java.lang.Object(List(EOC, o1577, o1496)))
1872_0_countMetaList_InvokeMethod(EOS(STATIC_1872), java.lang.Object(List(EOC, NULL, NULL)), java.lang.Object(List(EOC, NULL, NULL)), o1576, java.lang.Object(List(EOC, o1577, o1496))) → 1888_0_<init>_Load(EOS(STATIC_1888), java.lang.Object(List(EOC, NULL, NULL)), java.lang.Object(List(EOC, NULL, NULL)), o1576, java.lang.Object(List(EOC, o1577, o1496)), java.lang.Object(List(EOC, NULL, NULL)), o1576, java.lang.Object(List(EOC, o1577, o1496)))
1888_0_<init>_Load(EOS(STATIC_1888), java.lang.Object(List(EOC, NULL, NULL)), java.lang.Object(List(EOC, NULL, NULL)), o1576, java.lang.Object(List(EOC, o1577, o1496)), java.lang.Object(List(EOC, NULL, NULL)), o1576, java.lang.Object(List(EOC, o1577, o1496))) → 1924_0_<init>_InvokeMethod(EOS(STATIC_1924), java.lang.Object(List(EOC, NULL, NULL)), java.lang.Object(List(EOC, NULL, NULL)), o1576, java.lang.Object(List(EOC, o1577, o1496)), java.lang.Object(List(EOC, NULL, NULL)), o1576, java.lang.Object(List(EOC, o1577, o1496)), java.lang.Object(List(EOC, NULL, NULL)))
1924_0_<init>_InvokeMethod(EOS(STATIC_1924), java.lang.Object(List(EOC, NULL, NULL)), java.lang.Object(List(EOC, NULL, NULL)), o1576, java.lang.Object(List(EOC, o1577, o1496)), java.lang.Object(List(EOC, NULL, NULL)), o1576, java.lang.Object(List(EOC, o1577, o1496)), java.lang.Object(List(EOC, NULL, NULL))) → 1947_0_<init>_Load(EOS(STATIC_1947), java.lang.Object(List(EOC, NULL, NULL)), java.lang.Object(List(EOC, NULL, NULL)), o1576, java.lang.Object(List(EOC, o1577, o1496)), java.lang.Object(List(EOC, NULL, NULL)), o1576, java.lang.Object(List(EOC, o1577, o1496)))
1947_0_<init>_Load(EOS(STATIC_1947), java.lang.Object(List(EOC, NULL, NULL)), java.lang.Object(List(EOC, NULL, NULL)), o1576, java.lang.Object(List(EOC, o1577, o1496)), java.lang.Object(List(EOC, NULL, NULL)), o1576, java.lang.Object(List(EOC, o1577, o1496))) → 1984_0_<init>_Load(EOS(STATIC_1984), java.lang.Object(List(EOC, NULL, NULL)), java.lang.Object(List(EOC, NULL, NULL)), o1576, java.lang.Object(List(EOC, o1577, o1496)), java.lang.Object(List(EOC, NULL, NULL)), o1576, java.lang.Object(List(EOC, o1577, o1496)), java.lang.Object(List(EOC, NULL, NULL)))
1984_0_<init>_Load(EOS(STATIC_1984), java.lang.Object(List(EOC, NULL, NULL)), java.lang.Object(List(EOC, NULL, NULL)), o1576, java.lang.Object(List(EOC, o1577, o1496)), java.lang.Object(List(EOC, NULL, NULL)), o1576, java.lang.Object(List(EOC, o1577, o1496)), java.lang.Object(List(EOC, NULL, NULL))) → 1994_0_<init>_FieldAccess(EOS(STATIC_1994), java.lang.Object(List(EOC, NULL, NULL)), java.lang.Object(List(EOC, NULL, NULL)), o1576, java.lang.Object(List(EOC, o1577, o1496)), java.lang.Object(List(EOC, NULL, NULL)), java.lang.Object(List(EOC, o1577, o1496)), java.lang.Object(List(EOC, NULL, NULL)), o1576)
1994_0_<init>_FieldAccess(EOS(STATIC_1994), java.lang.Object(List(EOC, NULL, NULL)), java.lang.Object(List(EOC, NULL, NULL)), o1576, java.lang.Object(List(EOC, o1577, o1496)), java.lang.Object(List(EOC, NULL, NULL)), java.lang.Object(List(EOC, o1577, o1496)), java.lang.Object(List(EOC, NULL, NULL)), o1576) → 2016_0_<init>_Load(EOS(STATIC_2016), java.lang.Object(List(EOC, o1576, NULL)), java.lang.Object(List(EOC, o1576, NULL)), o1576, java.lang.Object(List(EOC, o1577, o1496)), java.lang.Object(List(EOC, o1576, NULL)), java.lang.Object(List(EOC, o1577, o1496)))
2016_0_<init>_Load(EOS(STATIC_2016), java.lang.Object(List(EOC, o1576, NULL)), java.lang.Object(List(EOC, o1576, NULL)), o1576, java.lang.Object(List(EOC, o1577, o1496)), java.lang.Object(List(EOC, o1576, NULL)), java.lang.Object(List(EOC, o1577, o1496))) → 2027_0_<init>_Load(EOS(STATIC_2027), java.lang.Object(List(EOC, o1576, NULL)), java.lang.Object(List(EOC, o1576, NULL)), o1576, java.lang.Object(List(EOC, o1577, o1496)), java.lang.Object(List(EOC, o1577, o1496)), java.lang.Object(List(EOC, o1576, NULL)))
2027_0_<init>_Load(EOS(STATIC_2027), java.lang.Object(List(EOC, o1576, NULL)), java.lang.Object(List(EOC, o1576, NULL)), o1576, java.lang.Object(List(EOC, o1577, o1496)), java.lang.Object(List(EOC, o1577, o1496)), java.lang.Object(List(EOC, o1576, NULL))) → 2049_0_<init>_FieldAccess(EOS(STATIC_2049), java.lang.Object(List(EOC, o1576, NULL)), java.lang.Object(List(EOC, o1576, NULL)), o1576, java.lang.Object(List(EOC, o1577, o1496)), java.lang.Object(List(EOC, o1576, NULL)), java.lang.Object(List(EOC, o1577, o1496)))
2049_0_<init>_FieldAccess(EOS(STATIC_2049), java.lang.Object(List(EOC, o1576, NULL)), java.lang.Object(List(EOC, o1576, NULL)), o1576, java.lang.Object(List(EOC, o1577, o1496)), java.lang.Object(List(EOC, o1576, NULL)), java.lang.Object(List(EOC, o1577, o1496))) → 2091_0_<init>_Return(EOS(STATIC_2091), java.lang.Object(List(EOC, o1576, java.lang.Object(List(EOC, o1577, o1496)))), java.lang.Object(List(EOC, o1576, java.lang.Object(List(EOC, o1577, o1496)))), o1576, java.lang.Object(List(EOC, o1577, o1496)))
2091_0_<init>_Return(EOS(STATIC_2091), java.lang.Object(List(EOC, o1576, java.lang.Object(List(EOC, o1577, o1496)))), java.lang.Object(List(EOC, o1576, java.lang.Object(List(EOC, o1577, o1496)))), o1576, java.lang.Object(List(EOC, o1577, o1496))) → 2102_0_countMetaList_Store(EOS(STATIC_2102), java.lang.Object(List(EOC, o1576, java.lang.Object(List(EOC, o1577, o1496)))))
2102_0_countMetaList_Store(EOS(STATIC_2102), java.lang.Object(List(EOC, o1576, java.lang.Object(List(EOC, o1577, o1496))))) → 2121_0_countMetaList_ConstantStackPush(EOS(STATIC_2121), java.lang.Object(List(EOC, o1576, java.lang.Object(List(EOC, o1577, o1496)))))
2121_0_countMetaList_ConstantStackPush(EOS(STATIC_2121), java.lang.Object(List(EOC, o1576, java.lang.Object(List(EOC, o1577, o1496))))) → 2130_0_countMetaList_Load(EOS(STATIC_2130), java.lang.Object(List(EOC, o1576, java.lang.Object(List(EOC, o1577, o1496)))), 1)
2130_0_countMetaList_Load(EOS(STATIC_2130), java.lang.Object(List(EOC, o1576, java.lang.Object(List(EOC, o1577, o1496)))), matching1) → 2151_0_countMetaList_FieldAccess(EOS(STATIC_2151), 1, java.lang.Object(List(EOC, o1576, java.lang.Object(List(EOC, o1577, o1496))))) | =(matching1, 1)
2151_0_countMetaList_FieldAccess(EOS(STATIC_2151), matching1, java.lang.Object(List(EOC, o1576, java.lang.Object(List(EOC, o1577, o1496))))) → 2196_0_countMetaList_InvokeMethod(EOS(STATIC_2196), 1, java.lang.Object(List(EOC, o1577, o1496))) | =(matching1, 1)
2196_0_countMetaList_InvokeMethod(EOS(STATIC_2196), matching1, java.lang.Object(List(EOC, o1577, o1496))) → 2207_1_countMetaList_InvokeMethod(2207_0_countMetaList_Load(EOS(STATIC_2207), java.lang.Object(List(EOC, o1577, o1496))), 1, java.lang.Object(List(EOC, o1577, o1496))) | =(matching1, 1)
2207_0_countMetaList_Load(EOS(STATIC_2207), java.lang.Object(List(EOC, o1577, o1496))) → 2221_0_countMetaList_Load(EOS(STATIC_2221), java.lang.Object(List(EOC, o1577, o1496)))
2221_0_countMetaList_Load(EOS(STATIC_2221), java.lang.Object(List(EOC, o1577, o1496))) → 1621_0_countMetaList_Load(EOS(STATIC_1621), java.lang.Object(List(EOC, o1577, o1496)))
1621_0_countMetaList_Load(EOS(STATIC_1621), o1469) → 1626_0_countMetaList_NONNULL(EOS(STATIC_1626), o1469, o1469)
1678_0_countMetaList_CheckCast(EOS(STATIC_1678), java.lang.Object(List(EOC, java.lang.Object(o1513sub), o1496)), java.lang.Object(o1513sub)) → 1690_0_countMetaList_EQ(EOS(STATIC_1690), java.lang.Object(List(EOC, java.lang.Object(o1513sub), o1496)), 0)
1690_0_countMetaList_EQ(EOS(STATIC_1690), java.lang.Object(List(EOC, java.lang.Object(o1513sub), o1496)), matching1) → 1701_0_countMetaList_ConstantStackPush(EOS(STATIC_1701), java.lang.Object(List(EOC, java.lang.Object(o1513sub), o1496))) | =(matching1, 0)
1701_0_countMetaList_ConstantStackPush(EOS(STATIC_1701), java.lang.Object(List(EOC, java.lang.Object(o1513sub), o1496))) → 1712_0_countMetaList_Load(EOS(STATIC_1712), java.lang.Object(List(EOC, java.lang.Object(o1513sub), o1496)), 1)
1712_0_countMetaList_Load(EOS(STATIC_1712), java.lang.Object(List(EOC, java.lang.Object(o1513sub), o1496)), matching1) → 1719_0_countMetaList_FieldAccess(EOS(STATIC_1719), 1, java.lang.Object(List(EOC, java.lang.Object(o1513sub), o1496))) | =(matching1, 1)
1719_0_countMetaList_FieldAccess(EOS(STATIC_1719), matching1, java.lang.Object(List(EOC, java.lang.Object(o1513sub), o1496))) → 1729_0_countMetaList_InvokeMethod(EOS(STATIC_1729), 1, o1496) | =(matching1, 1)
1729_0_countMetaList_InvokeMethod(EOS(STATIC_1729), matching1, o1496) → 1739_1_countMetaList_InvokeMethod(1739_0_countMetaList_Load(EOS(STATIC_1739), o1496), 1, o1496) | =(matching1, 1)
1739_0_countMetaList_Load(EOS(STATIC_1739), o1496) → 1747_0_countMetaList_Load(EOS(STATIC_1747), o1496)
1747_0_countMetaList_Load(EOS(STATIC_1747), o1496) → 1621_0_countMetaList_Load(EOS(STATIC_1621), o1496)
1666_0_countMetaList_CheckCast(EOS(STATIC_1666), java.lang.Object(List(EOC, NULL, o1496)), NULL) → 1679_0_countMetaList_EQ(EOS(STATIC_1679), java.lang.Object(List(EOC, NULL, o1496)), 0)
1679_0_countMetaList_EQ(EOS(STATIC_1679), java.lang.Object(List(EOC, NULL, o1496)), matching1) → 1692_0_countMetaList_ConstantStackPush(EOS(STATIC_1692), java.lang.Object(List(EOC, NULL, o1496))) | =(matching1, 0)
1692_0_countMetaList_ConstantStackPush(EOS(STATIC_1692), java.lang.Object(List(EOC, NULL, o1496))) → 1703_0_countMetaList_Load(EOS(STATIC_1703), java.lang.Object(List(EOC, NULL, o1496)), 1)
1703_0_countMetaList_Load(EOS(STATIC_1703), java.lang.Object(List(EOC, NULL, o1496)), matching1) → 1713_0_countMetaList_FieldAccess(EOS(STATIC_1713), 1, java.lang.Object(List(EOC, NULL, o1496))) | =(matching1, 1)
1713_0_countMetaList_FieldAccess(EOS(STATIC_1713), matching1, java.lang.Object(List(EOC, NULL, o1496))) → 1721_0_countMetaList_InvokeMethod(EOS(STATIC_1721), 1, o1496) | =(matching1, 1)
1721_0_countMetaList_InvokeMethod(EOS(STATIC_1721), matching1, o1496) → 1730_1_countMetaList_InvokeMethod(1730_0_countMetaList_Load(EOS(STATIC_1730), o1496), 1, o1496) | =(matching1, 1)
1730_0_countMetaList_Load(EOS(STATIC_1730), o1496) → 1740_0_countMetaList_Load(EOS(STATIC_1740), o1496)
1740_0_countMetaList_Load(EOS(STATIC_1740), o1496) → 1621_0_countMetaList_Load(EOS(STATIC_1621), o1496)
R rules:
1626_0_countMetaList_NONNULL(EOS(STATIC_1626), NULL, NULL) → 1632_0_countMetaList_NONNULL(EOS(STATIC_1632), NULL, NULL)
1632_0_countMetaList_NONNULL(EOS(STATIC_1632), NULL, NULL) → 1638_0_countMetaList_ConstantStackPush(EOS(STATIC_1638), NULL)
1638_0_countMetaList_ConstantStackPush(EOS(STATIC_1638), NULL) → 1646_0_countMetaList_Return(EOS(STATIC_1646), NULL, 0)
1730_1_countMetaList_InvokeMethod(1646_0_countMetaList_Return(EOS(STATIC_1646), NULL, matching1), matching2, NULL) → 1768_0_countMetaList_Return(EOS(STATIC_1768), 1, NULL, NULL, 0) | &&(=(matching1, 0), =(matching2, 1))
1730_1_countMetaList_InvokeMethod(2507_0_countMetaList_Return(EOS(STATIC_2507), i1140), matching1, o1496) → 2528_0_countMetaList_Return(EOS(STATIC_2528), 1, java.lang.Object(List(EOC, o2860, o2859)), i1140) | =(matching1, 1)
1739_1_countMetaList_InvokeMethod(1646_0_countMetaList_Return(EOS(STATIC_1646), NULL, matching1), matching2, NULL) → 1778_0_countMetaList_Return(EOS(STATIC_1778), 1, NULL, NULL, 0) | &&(=(matching1, 0), =(matching2, 1))
1739_1_countMetaList_InvokeMethod(2507_0_countMetaList_Return(EOS(STATIC_2507), i1140), matching1, o1496) → 2531_0_countMetaList_Return(EOS(STATIC_2531), 1, java.lang.Object(List(EOC, o2860, o2859)), i1140) | =(matching1, 1)
1768_0_countMetaList_Return(EOS(STATIC_1768), matching1, NULL, NULL, matching2) → 1779_0_countMetaList_IntArithmetic(EOS(STATIC_1779), 1, 0) | &&(=(matching1, 1), =(matching2, 0))
1778_0_countMetaList_Return(EOS(STATIC_1778), matching1, NULL, NULL, matching2) → 1790_0_countMetaList_IntArithmetic(EOS(STATIC_1790), 1, 0) | &&(=(matching1, 1), =(matching2, 0))
1779_0_countMetaList_IntArithmetic(EOS(STATIC_1779), matching1, matching2) → 2502_0_countMetaList_IntArithmetic(EOS(STATIC_2502), 1, 0) | &&(=(matching1, 1), =(matching2, 0))
1790_0_countMetaList_IntArithmetic(EOS(STATIC_1790), matching1, matching2) → 2502_0_countMetaList_IntArithmetic(EOS(STATIC_2502), 1, 0) | &&(=(matching1, 1), =(matching2, 0))
1859_0_countMetaList_Return(EOS(STATIC_1859), matching1, java.lang.Object(List(EOC, o1649, NULL)), matching2) → 1961_0_countMetaList_Return(EOS(STATIC_1961), 1, java.lang.Object(List(EOC, o1649, NULL)), 1) | &&(=(matching1, 1), =(matching2, 1))
1864_0_countMetaList_Return(EOS(STATIC_1864), matching1, java.lang.Object(List(EOC, o1660, NULL)), matching2) → 1971_0_countMetaList_Return(EOS(STATIC_1971), 1, java.lang.Object(List(EOC, o1660, NULL)), 1) | &&(=(matching1, 1), =(matching2, 1))
1961_0_countMetaList_Return(EOS(STATIC_1961), matching1, java.lang.Object(List(EOC, o1802, o1801)), i703) → 2066_0_countMetaList_Return(EOS(STATIC_2066), 1, java.lang.Object(List(EOC, o1802, o1801)), i703) | =(matching1, 1)
1971_0_countMetaList_Return(EOS(STATIC_1971), matching1, java.lang.Object(List(EOC, o1834, o1833)), i712) → 2077_0_countMetaList_Return(EOS(STATIC_2077), 1, java.lang.Object(List(EOC, o1834, o1833)), i712) | =(matching1, 1)
2066_0_countMetaList_Return(EOS(STATIC_2066), matching1, java.lang.Object(List(EOC, o1995, o1994)), i765) → 2169_0_countMetaList_Return(EOS(STATIC_2169), 1, java.lang.Object(List(EOC, o1995, o1994)), i765) | =(matching1, 1)
2077_0_countMetaList_Return(EOS(STATIC_2077), matching1, java.lang.Object(List(EOC, o2031, o2030)), i775) → 2180_0_countMetaList_Return(EOS(STATIC_2180), 1, java.lang.Object(List(EOC, o2031, o2030)), i775) | =(matching1, 1)
2169_0_countMetaList_Return(EOS(STATIC_2169), matching1, java.lang.Object(List(EOC, o2198, o2197)), i839) → 2275_0_countMetaList_Return(EOS(STATIC_2275), 1, java.lang.Object(List(EOC, o2198, o2197)), i839) | =(matching1, 1)
2180_0_countMetaList_Return(EOS(STATIC_2180), matching1, java.lang.Object(List(EOC, o2232, o2231)), i849) → 2286_0_countMetaList_Return(EOS(STATIC_2286), 1, java.lang.Object(List(EOC, o2232, o2231)), i849) | =(matching1, 1)
2207_1_countMetaList_InvokeMethod(2507_0_countMetaList_Return(EOS(STATIC_2507), i1140), matching1, java.lang.Object(List(EOC, o1577, o1496))) → 2533_0_countMetaList_Return(EOS(STATIC_2533), 1, java.lang.Object(List(EOC, o2860, o2859)), i1140) | =(matching1, 1)
2275_0_countMetaList_Return(EOS(STATIC_2275), matching1, java.lang.Object(List(EOC, o2399, o2398)), i909) → 2382_0_countMetaList_Return(EOS(STATIC_2382), 1, java.lang.Object(List(EOC, o2399, o2398)), i909) | =(matching1, 1)
2286_0_countMetaList_Return(EOS(STATIC_2286), matching1, java.lang.Object(List(EOC, o2436, o2435)), i919) → 2390_0_countMetaList_Return(EOS(STATIC_2390), 1, java.lang.Object(List(EOC, o2436, o2435)), i919) | =(matching1, 1)
2311_0_countMetaList_Return(EOS(STATIC_2311), matching1, java.lang.Object(List(EOC, NULL, o2497)), i944) → 2472_0_countMetaList_Return(EOS(STATIC_2472), 1, java.lang.Object(List(EOC, NULL, o2497)), i944) | =(matching1, 1)
2382_0_countMetaList_Return(EOS(STATIC_2382), matching1, java.lang.Object(List(EOC, o2634, o2633)), i986) → 2396_0_countMetaList_IntArithmetic(EOS(STATIC_2396), 1, i986) | =(matching1, 1)
2390_0_countMetaList_Return(EOS(STATIC_2390), matching1, java.lang.Object(List(EOC, o2662, o2661)), i992) → 2399_0_countMetaList_IntArithmetic(EOS(STATIC_2399), 1, i992) | =(matching1, 1)
2396_0_countMetaList_IntArithmetic(EOS(STATIC_2396), matching1, i986) → 2502_0_countMetaList_IntArithmetic(EOS(STATIC_2502), 1, i986) | =(matching1, 1)
2399_0_countMetaList_IntArithmetic(EOS(STATIC_2399), matching1, i992) → 2502_0_countMetaList_IntArithmetic(EOS(STATIC_2502), 1, i992) | =(matching1, 1)
2472_0_countMetaList_Return(EOS(STATIC_2472), matching1, java.lang.Object(List(EOC, NULL, o2813)), i1068) → 2489_0_countMetaList_Return(EOS(STATIC_2489), 1, java.lang.Object(List(EOC, NULL, o2813)), i1068) | =(matching1, 1)
2489_0_countMetaList_Return(EOS(STATIC_2489), matching1, java.lang.Object(List(EOC, o2860, o2859)), i1094) → 2502_0_countMetaList_IntArithmetic(EOS(STATIC_2502), 1, i1094) | =(matching1, 1)
2502_0_countMetaList_IntArithmetic(EOS(STATIC_2502), matching1, i1094) → 2507_0_countMetaList_Return(EOS(STATIC_2507), +(1, i1094)) | =(matching1, 1)
2528_0_countMetaList_Return(EOS(STATIC_2528), matching1, java.lang.Object(List(EOC, o2860, o2859)), i1140) → 2382_0_countMetaList_Return(EOS(STATIC_2382), 1, java.lang.Object(List(EOC, o2860, o2859)), i1140) | =(matching1, 1)
2531_0_countMetaList_Return(EOS(STATIC_2531), matching1, java.lang.Object(List(EOC, o2860, o2859)), i1140) → 2390_0_countMetaList_Return(EOS(STATIC_2390), 1, java.lang.Object(List(EOC, o2860, o2859)), i1140) | =(matching1, 1)
2533_0_countMetaList_Return(EOS(STATIC_2533), matching1, java.lang.Object(List(EOC, o2860, o2859)), i1140) → 2489_0_countMetaList_Return(EOS(STATIC_2489), 1, java.lang.Object(List(EOC, o2860, o2859)), i1140) | =(matching1, 1)

Combined rules. Obtained 3 conditional rules for P and 6 conditional rules for R.

P rules:
1626_0_countMetaList_NONNULL(EOS(STATIC_1626), java.lang.Object(List(EOC, java.lang.Object(List(EOC, x0, x1)), x2)), java.lang.Object(List(EOC, java.lang.Object(List(EOC, x0, x1)), x2))) → 2207_1_countMetaList_InvokeMethod(1626_0_countMetaList_NONNULL(EOS(STATIC_1626), java.lang.Object(List(EOC, x1, x2)), java.lang.Object(List(EOC, x1, x2))), 1, java.lang.Object(List(EOC, x1, x2)))
1626_0_countMetaList_NONNULL(EOS(STATIC_1626), java.lang.Object(List(EOC, java.lang.Object(x0), x1)), java.lang.Object(List(EOC, java.lang.Object(x0), x1))) → 1739_1_countMetaList_InvokeMethod(1626_0_countMetaList_NONNULL(EOS(STATIC_1626), x1, x1), 1, x1)
1626_0_countMetaList_NONNULL(EOS(STATIC_1626), java.lang.Object(List(EOC, NULL, x0)), java.lang.Object(List(EOC, NULL, x0))) → 1730_1_countMetaList_InvokeMethod(1626_0_countMetaList_NONNULL(EOS(STATIC_1626), x0, x0), 1, x0)
R rules:
1626_0_countMetaList_NONNULL(EOS(STATIC_1626), NULL, NULL) → 1646_0_countMetaList_Return(EOS(STATIC_1646), NULL, 0)
1730_1_countMetaList_InvokeMethod(1646_0_countMetaList_Return(EOS(STATIC_1646), NULL, 0), 1, NULL) → 2507_0_countMetaList_Return(EOS(STATIC_2507), 1)
1739_1_countMetaList_InvokeMethod(1646_0_countMetaList_Return(EOS(STATIC_1646), NULL, 0), 1, NULL) → 2507_0_countMetaList_Return(EOS(STATIC_2507), 1)
1730_1_countMetaList_InvokeMethod(2507_0_countMetaList_Return(EOS(STATIC_2507), x0), 1, x2) → 2507_0_countMetaList_Return(EOS(STATIC_2507), +(1, x0))
1739_1_countMetaList_InvokeMethod(2507_0_countMetaList_Return(EOS(STATIC_2507), x0), 1, x2) → 2507_0_countMetaList_Return(EOS(STATIC_2507), +(1, x0))
2207_1_countMetaList_InvokeMethod(2507_0_countMetaList_Return(EOS(STATIC_2507), x0), 1, java.lang.Object(List(EOC, x2, x3))) → 2507_0_countMetaList_Return(EOS(STATIC_2507), +(1, x0))

Filtered ground terms:

1730_1_countMetaList_InvokeMethod(x1, x2, x3) → 1730_1_countMetaList_InvokeMethod(x1, x3)
1626_0_countMetaList_NONNULL(x1, x2, x3) → 1626_0_countMetaList_NONNULL(x2, x3)
List(x1, x2, x3) → List(x2, x3)
1739_1_countMetaList_InvokeMethod(x1, x2, x3) → 1739_1_countMetaList_InvokeMethod(x1, x3)
2207_1_countMetaList_InvokeMethod(x1, x2, x3) → 2207_1_countMetaList_InvokeMethod(x1, x3)
2507_0_countMetaList_Return(x1, x2) → 2507_0_countMetaList_Return(x2)
1646_0_countMetaList_Return(x1, x2, x3) → 1646_0_countMetaList_Return

Filtered duplicate args:

1626_0_countMetaList_NONNULL(x1, x2) → 1626_0_countMetaList_NONNULL(x2)

Filtered unneeded arguments:

2207_1_countMetaList_InvokeMethod(x1, x2) → 2207_1_countMetaList_InvokeMethod(x1)

Combined rules. Obtained 3 conditional rules for P and 6 conditional rules for R.

P rules:
1626_0_countMetaList_NONNULL(java.lang.Object(List(java.lang.Object(List(x0, x1)), x2))) → 2207_1_countMetaList_InvokeMethod(1626_0_countMetaList_NONNULL(java.lang.Object(List(x1, x2))))
1626_0_countMetaList_NONNULL(java.lang.Object(List(java.lang.Object(x0), x1))) → 1739_1_countMetaList_InvokeMethod(1626_0_countMetaList_NONNULL(x1), x1)
1626_0_countMetaList_NONNULL(java.lang.Object(List(NULL, x0))) → 1730_1_countMetaList_InvokeMethod(1626_0_countMetaList_NONNULL(x0), x0)
R rules:
1626_0_countMetaList_NONNULL(NULL) → 1646_0_countMetaList_Return
1730_1_countMetaList_InvokeMethod(1646_0_countMetaList_Return, NULL) → 2507_0_countMetaList_Return(1)
1739_1_countMetaList_InvokeMethod(1646_0_countMetaList_Return, NULL) → 2507_0_countMetaList_Return(1)
1730_1_countMetaList_InvokeMethod(2507_0_countMetaList_Return(x0), x2) → 2507_0_countMetaList_Return(+(1, x0))
1739_1_countMetaList_InvokeMethod(2507_0_countMetaList_Return(x0), x2) → 2507_0_countMetaList_Return(+(1, x0))
2207_1_countMetaList_InvokeMethod(2507_0_countMetaList_Return(x0)) → 2507_0_countMetaList_Return(+(1, x0))

Performed bisimulation on rules. Used the following equivalence classes: {[1730_1_countMetaList_InvokeMethod_2, 1739_1_countMetaList_InvokeMethod_2]=1730_1_countMetaList_InvokeMethod_2}

Finished conversion. Obtained 3 rules for P and 4 rules for R. System has predefined symbols.

P rules:
1626_0_COUNTMETALIST_NONNULL(java.lang.Object(List(java.lang.Object(List(x0, x1)), x2))) → 1626_0_COUNTMETALIST_NONNULL(java.lang.Object(List(x1, x2)))
1626_0_COUNTMETALIST_NONNULL(java.lang.Object(List(java.lang.Object(x0), x1))) → 1626_0_COUNTMETALIST_NONNULL(x1)
1626_0_COUNTMETALIST_NONNULL(java.lang.Object(List(NULL, x0))) → 1626_0_COUNTMETALIST_NONNULL(x0)
R rules:
1626_0_countMetaList_NONNULL(NULL) → 1646_0_countMetaList_Return
1730_1_countMetaList_InvokeMethod(1646_0_countMetaList_Return, NULL) → 2507_0_countMetaList_Return(1)
1730_1_countMetaList_InvokeMethod(2507_0_countMetaList_Return(x0), x2) → 2507_0_countMetaList_Return(+(1, x0))
2207_1_countMetaList_InvokeMethod(2507_0_countMetaList_Return(x0)) → 2507_0_countMetaList_Return(+(1, x0))

(7) Obligation:

IDP problem:
The following function symbols are pre-defined:

!=	~	Neq: (Integer, Integer) -> Boolean
*	~	Mul: (Integer, Integer) -> Integer
>=	~	Ge: (Integer, Integer) -> Boolean
-1	~	UnaryMinus: (Integer) -> Integer
\|	~	Bwor: (Integer, Integer) -> Integer
/	~	Div: (Integer, Integer) -> Integer
=	~	Eq: (Integer, Integer) -> Boolean
	~	Bwxor: (Integer, Integer) -> Integer
\|\|	~	Lor: (Boolean, Boolean) -> Boolean
!	~	Lnot: (Boolean) -> Boolean
<	~	Lt: (Integer, Integer) -> Boolean
-	~	Sub: (Integer, Integer) -> Integer
<=	~	Le: (Integer, Integer) -> Boolean
>	~	Gt: (Integer, Integer) -> Boolean
~	~	Bwnot: (Integer) -> Integer
%	~	Mod: (Integer, Integer) -> Integer
&	~	Bwand: (Integer, Integer) -> Integer
+	~	Add: (Integer, Integer) -> Integer
&&	~	Land: (Boolean, Boolean) -> Boolean

The following domains are used:

Integer

The ITRS R consists of the following rules:
1626_0_countMetaList_NONNULL(NULL) → 1646_0_countMetaList_Return
1730_1_countMetaList_InvokeMethod(1646_0_countMetaList_Return, NULL) → 2507_0_countMetaList_Return(1)
1730_1_countMetaList_InvokeMethod(2507_0_countMetaList_Return(x0), x2) → 2507_0_countMetaList_Return(1 + x0)
2207_1_countMetaList_InvokeMethod(2507_0_countMetaList_Return(x0)) → 2507_0_countMetaList_Return(1 + x0)

The integer pair graph contains the following rules and edges:
(0): 1626_0_COUNTMETALIST_NONNULL(java.lang.Object(List(java.lang.Object(List(x0[0], x1[0])), x2[0]))) → 1626_0_COUNTMETALIST_NONNULL(java.lang.Object(List(x1[0], x2[0])))
(1): 1626_0_COUNTMETALIST_NONNULL(java.lang.Object(List(java.lang.Object(x0[1]), x1[1]))) → 1626_0_COUNTMETALIST_NONNULL(x1[1])
(2): 1626_0_COUNTMETALIST_NONNULL(java.lang.Object(List(NULL, x0[2]))) → 1626_0_COUNTMETALIST_NONNULL(x0[2])

(0) -> (0), if (java.lang.Object(List(x1[0], x2[0])) →^* java.lang.Object(List(java.lang.Object(List(x0[0]', x1[0]')), x2[0]')))

(0) -> (1), if (java.lang.Object(List(x1[0], x2[0])) →^* java.lang.Object(List(java.lang.Object(x0[1]), x1[1])))

(0) -> (2), if (java.lang.Object(List(x1[0], x2[0])) →^* java.lang.Object(List(NULL, x0[2])))

(1) -> (0), if (x1[1] →^* java.lang.Object(List(java.lang.Object(List(x0[0], x1[0])), x2[0])))

(1) -> (1), if (x1[1] →^* java.lang.Object(List(java.lang.Object(x0[1]'), x1[1]')))

(1) -> (2), if (x1[1] →^* java.lang.Object(List(NULL, x0[2])))

(2) -> (0), if (x0[2] →^* java.lang.Object(List(java.lang.Object(List(x0[0], x1[0])), x2[0])))

(2) -> (1), if (x0[2] →^* java.lang.Object(List(java.lang.Object(x0[1]), x1[1])))

(2) -> (2), if (x0[2] →^* java.lang.Object(List(NULL, x0[2]')))

The set Q consists of the following terms:
1626_0_countMetaList_NONNULL(NULL)
1730_1_countMetaList_InvokeMethod(1646_0_countMetaList_Return, NULL)
1730_1_countMetaList_InvokeMethod(2507_0_countMetaList_Return(x0), x1)
2207_1_countMetaList_InvokeMethod(2507_0_countMetaList_Return(x0))

(8) IDPtoQDPProof (SOUND transformation)

Represented integers and predefined function symbols by Terms

(9) Obligation:

Q DP problem:
The TRS P consists of the following rules:

1626_0_COUNTMETALIST_NONNULL(java.lang.Object(List(java.lang.Object(List(x0[0], x1[0])), x2[0]))) → 1626_0_COUNTMETALIST_NONNULL(java.lang.Object(List(x1[0], x2[0])))
1626_0_COUNTMETALIST_NONNULL(java.lang.Object(List(java.lang.Object(x0[1]), x1[1]))) → 1626_0_COUNTMETALIST_NONNULL(x1[1])
1626_0_COUNTMETALIST_NONNULL(java.lang.Object(List(NULL, x0[2]))) → 1626_0_COUNTMETALIST_NONNULL(x0[2])

The TRS R consists of the following rules:

1626_0_countMetaList_NONNULL(NULL) → 1646_0_countMetaList_Return
1730_1_countMetaList_InvokeMethod(1646_0_countMetaList_Return, NULL) → 2507_0_countMetaList_Return(pos(s(0)))
1730_1_countMetaList_InvokeMethod(2507_0_countMetaList_Return(x0), x2) → 2507_0_countMetaList_Return(plus_int(pos(s(0)), x0))
2207_1_countMetaList_InvokeMethod(2507_0_countMetaList_Return(x0)) → 2507_0_countMetaList_Return(plus_int(pos(s(0)), x0))
plus_int(pos(x), neg(y)) → minus_nat(x, y)
plus_int(neg(x), pos(y)) → minus_nat(y, x)
plus_int(neg(x), neg(y)) → neg(plus_nat(x, y))
plus_int(pos(x), pos(y)) → pos(plus_nat(x, y))
plus_nat(0, x) → x
plus_nat(s(x), y) → s(plus_nat(x, y))
minus_nat(0, 0) → pos(0)
minus_nat(0, s(y)) → neg(s(y))
minus_nat(s(x), 0) → pos(s(x))
minus_nat(s(x), s(y)) → minus_nat(x, y)

The set Q consists of the following terms:

1626_0_countMetaList_NONNULL(NULL)
1730_1_countMetaList_InvokeMethod(1646_0_countMetaList_Return, NULL)
1730_1_countMetaList_InvokeMethod(2507_0_countMetaList_Return(x0), x1)
2207_1_countMetaList_InvokeMethod(2507_0_countMetaList_Return(x0))
plus_int(pos(x0), neg(x1))
plus_int(neg(x0), pos(x1))
plus_int(neg(x0), neg(x1))
plus_int(pos(x0), pos(x1))
plus_nat(0, x0)
plus_nat(s(x0), x1)
minus_nat(0, 0)
minus_nat(0, s(x0))
minus_nat(s(x0), 0)
minus_nat(s(x0), s(x1))

We have to consider all minimal (P,Q,R)-chains.

(10) UsableRulesProof (EQUIVALENT transformation)

As all Q-normal forms are R-normal forms we are in the innermost case. Hence, by the usable rules processor [LPAR04] we can delete all non-usable rules [FROCOS05] from R.

(11) Obligation:

Q DP problem:
The TRS P consists of the following rules:

1626_0_COUNTMETALIST_NONNULL(java.lang.Object(List(java.lang.Object(List(x0[0], x1[0])), x2[0]))) → 1626_0_COUNTMETALIST_NONNULL(java.lang.Object(List(x1[0], x2[0])))
1626_0_COUNTMETALIST_NONNULL(java.lang.Object(List(java.lang.Object(x0[1]), x1[1]))) → 1626_0_COUNTMETALIST_NONNULL(x1[1])
1626_0_COUNTMETALIST_NONNULL(java.lang.Object(List(NULL, x0[2]))) → 1626_0_COUNTMETALIST_NONNULL(x0[2])

R is empty.
The set Q consists of the following terms:

1626_0_countMetaList_NONNULL(NULL)
1730_1_countMetaList_InvokeMethod(1646_0_countMetaList_Return, NULL)
1730_1_countMetaList_InvokeMethod(2507_0_countMetaList_Return(x0), x1)
2207_1_countMetaList_InvokeMethod(2507_0_countMetaList_Return(x0))
plus_int(pos(x0), neg(x1))
plus_int(neg(x0), pos(x1))
plus_int(neg(x0), neg(x1))
plus_int(pos(x0), pos(x1))
plus_nat(0, x0)
plus_nat(s(x0), x1)
minus_nat(0, 0)
minus_nat(0, s(x0))
minus_nat(s(x0), 0)
minus_nat(s(x0), s(x1))

We have to consider all minimal (P,Q,R)-chains.

(12) QReductionProof (EQUIVALENT transformation)

We deleted the following terms from Q as each root-symbol of these terms does neither occur in P nor in R.[THIEMANN].

1626_0_countMetaList_NONNULL(NULL)
1730_1_countMetaList_InvokeMethod(1646_0_countMetaList_Return, NULL)
1730_1_countMetaList_InvokeMethod(2507_0_countMetaList_Return(x0), x1)
2207_1_countMetaList_InvokeMethod(2507_0_countMetaList_Return(x0))
plus_int(pos(x0), neg(x1))
plus_int(neg(x0), pos(x1))
plus_int(neg(x0), neg(x1))
plus_int(pos(x0), pos(x1))
plus_nat(0, x0)
plus_nat(s(x0), x1)
minus_nat(0, 0)
minus_nat(0, s(x0))
minus_nat(s(x0), 0)
minus_nat(s(x0), s(x1))

(13) Obligation:

Q DP problem:
The TRS P consists of the following rules:

1626_0_COUNTMETALIST_NONNULL(java.lang.Object(List(java.lang.Object(List(x0[0], x1[0])), x2[0]))) → 1626_0_COUNTMETALIST_NONNULL(java.lang.Object(List(x1[0], x2[0])))
1626_0_COUNTMETALIST_NONNULL(java.lang.Object(List(java.lang.Object(x0[1]), x1[1]))) → 1626_0_COUNTMETALIST_NONNULL(x1[1])
1626_0_COUNTMETALIST_NONNULL(java.lang.Object(List(NULL, x0[2]))) → 1626_0_COUNTMETALIST_NONNULL(x0[2])

R is empty.
Q is empty.
We have to consider all minimal (P,Q,R)-chains.

(14) UsableRulesReductionPairsProof (EQUIVALENT transformation)

By using the usable rules with reduction pair processor [LPAR04] with a polynomial ordering [POLO], all dependency pairs and the corresponding usable rules [FROCOS05] can be oriented non-strictly. All non-usable rules are removed, and those dependency pairs and usable rules that have been oriented strictly or contain non-usable symbols in their left-hand side are removed as well.

The following dependency pairs can be deleted:

1626_0_COUNTMETALIST_NONNULL(java.lang.Object(List(NULL, x0[2]))) → 1626_0_COUNTMETALIST_NONNULL(x0[2])

No rules are removed from R.

Used ordering: POLO with Polynomial interpretation [POLO]:

POL(1626_0_COUNTMETALIST_NONNULL(x₁)) = 2·x₁
POL(List(x₁, x₂)) = x₁ + 2·x₂
POL(NULL) = 0
POL(java.lang.Object(x₁)) = 2·x₁

(15) Obligation:

Q DP problem:
The TRS P consists of the following rules:

1626_0_COUNTMETALIST_NONNULL(java.lang.Object(List(java.lang.Object(List(x0[0], x1[0])), x2[0]))) → 1626_0_COUNTMETALIST_NONNULL(java.lang.Object(List(x1[0], x2[0])))
1626_0_COUNTMETALIST_NONNULL(java.lang.Object(List(java.lang.Object(x0[1]), x1[1]))) → 1626_0_COUNTMETALIST_NONNULL(x1[1])

R is empty.
Q is empty.
We have to consider all minimal (P,Q,R)-chains.

(16) MRRProof (EQUIVALENT transformation)

By using the rule removal processor [LPAR04] with the following ordering, at least one Dependency Pair or term rewrite system rule of this QDP problem can be strictly oriented.
Strictly oriented dependency pairs:

1626_0_COUNTMETALIST_NONNULL(java.lang.Object(List(java.lang.Object(List(x0[0], x1[0])), x2[0]))) → 1626_0_COUNTMETALIST_NONNULL(java.lang.Object(List(x1[0], x2[0])))
1626_0_COUNTMETALIST_NONNULL(java.lang.Object(List(java.lang.Object(x0[1]), x1[1]))) → 1626_0_COUNTMETALIST_NONNULL(x1[1])

Used ordering: Polynomial interpretation [POLO]:

POL(1626_0_COUNTMETALIST_NONNULL(x₁)) = 2·x₁
POL(List(x₁, x₂)) = 2 + 2·x₁ + 2·x₂
POL(java.lang.Object(x₁)) = 2 + 2·x₁

(17) Obligation:

Q DP problem:
P is empty.
R is empty.
Q is empty.
We have to consider all minimal (P,Q,R)-chains.

(18) PisEmptyProof (EQUIVALENT transformation)

The TRS P is empty. Hence, there is no (P,Q,R) chain.

(19) YES

(20) Obligation:

SCC of termination graph based on JBC Program.
SCC contains nodes from the following methods: CountMetaListRec.createMetaList()LList;
SCC calls the following helper methods:
Performed SCC analyses: UsedFieldsAnalysis

(21) SCCToIDPv1Proof (SOUND transformation)

Transformed FIGraph SCCs to IDPs. Log:

Generated 69 rules for P and 0 rules for R.

P rules:
2682_0_createMetaList_Load(EOS(STATIC_2682), i79, i1246, i1246) → 2683_0_createMetaList_GE(EOS(STATIC_2683), i79, i1246, i1246, i79)
2683_0_createMetaList_GE(EOS(STATIC_2683), i79, i1246, i1246, i79) → 2686_0_createMetaList_GE(EOS(STATIC_2686), i79, i1246, i1246, i79)
2686_0_createMetaList_GE(EOS(STATIC_2686), i79, i1246, i1246, i79) → 2688_0_createMetaList_InvokeMethod(EOS(STATIC_2688), i79, i1246) | <(i1246, i79)
2688_0_createMetaList_InvokeMethod(EOS(STATIC_2688), i79, i1246) → 2691_0_random_FieldAccess(EOS(STATIC_2691), i79, i1246)
2691_0_random_FieldAccess(EOS(STATIC_2691), i79, i1246) → 2695_0_random_FieldAccess(EOS(STATIC_2695), i79, i1246)
2695_0_random_FieldAccess(EOS(STATIC_2695), i79, i1246) → 2699_0_random_ArrayAccess(EOS(STATIC_2699), i79, i1246)
2699_0_random_ArrayAccess(EOS(STATIC_2699), i79, i1246) → 2700_0_random_ArrayAccess(EOS(STATIC_2700), i79, i1246)
2700_0_random_ArrayAccess(EOS(STATIC_2700), i79, i1246) → 2703_0_random_Store(EOS(STATIC_2703), i79, i1246, o3109)
2703_0_random_Store(EOS(STATIC_2703), i79, i1246, o3109) → 2706_0_random_FieldAccess(EOS(STATIC_2706), i79, i1246, o3109)
2706_0_random_FieldAccess(EOS(STATIC_2706), i79, i1246, o3109) → 2707_0_random_ConstantStackPush(EOS(STATIC_2707), i79, i1246, o3109)
2707_0_random_ConstantStackPush(EOS(STATIC_2707), i79, i1246, o3109) → 2710_0_random_IntArithmetic(EOS(STATIC_2710), i79, i1246, o3109)
2710_0_random_IntArithmetic(EOS(STATIC_2710), i79, i1246, o3109) → 2713_0_random_FieldAccess(EOS(STATIC_2713), i79, i1246, o3109)
2713_0_random_FieldAccess(EOS(STATIC_2713), i79, i1246, o3109) → 2714_0_random_Load(EOS(STATIC_2714), i79, i1246, o3109)
2714_0_random_Load(EOS(STATIC_2714), i79, i1246, o3109) → 2719_0_random_InvokeMethod(EOS(STATIC_2719), i79, i1246, o3109)
2719_0_random_InvokeMethod(EOS(STATIC_2719), i79, i1246, java.lang.Object(o3127sub)) → 2721_0_random_InvokeMethod(EOS(STATIC_2721), i79, i1246, java.lang.Object(o3127sub))
2721_0_random_InvokeMethod(EOS(STATIC_2721), i79, i1246, java.lang.Object(o3127sub)) → 2724_0_length_Load(EOS(STATIC_2724), i79, i1246, java.lang.Object(o3127sub), java.lang.Object(o3127sub))
2724_0_length_Load(EOS(STATIC_2724), i79, i1246, java.lang.Object(o3127sub), java.lang.Object(o3127sub)) → 2732_0_length_FieldAccess(EOS(STATIC_2732), i79, i1246, java.lang.Object(o3127sub), java.lang.Object(o3127sub))
2732_0_length_FieldAccess(EOS(STATIC_2732), i79, i1246, java.lang.Object(java.lang.String(o3135sub, i1278)), java.lang.Object(java.lang.String(o3135sub, i1278))) → 2733_0_length_FieldAccess(EOS(STATIC_2733), i79, i1246, java.lang.Object(java.lang.String(o3135sub, i1278)), java.lang.Object(java.lang.String(o3135sub, i1278))) | &&(>=(i1278, 0), >=(i1279, 0))
2733_0_length_FieldAccess(EOS(STATIC_2733), i79, i1246, java.lang.Object(java.lang.String(o3135sub, i1278)), java.lang.Object(java.lang.String(o3135sub, i1278))) → 2738_0_length_Return(EOS(STATIC_2738), i79, i1246, java.lang.Object(java.lang.String(o3135sub, i1278)), i1278)
2738_0_length_Return(EOS(STATIC_2738), i79, i1246, java.lang.Object(java.lang.String(o3135sub, i1278)), i1278) → 2742_0_random_Return(EOS(STATIC_2742), i79, i1246, i1278)
2742_0_random_Return(EOS(STATIC_2742), i79, i1246, i1278) → 2744_0_createMetaList_Store(EOS(STATIC_2744), i79, i1246, i1278)
2744_0_createMetaList_Store(EOS(STATIC_2744), i79, i1246, i1278) → 2749_0_createMetaList_ConstantStackPush(EOS(STATIC_2749), i79, i1246, i1278)
2749_0_createMetaList_ConstantStackPush(EOS(STATIC_2749), i79, i1246, i1278) → 2753_0_createMetaList_Store(EOS(STATIC_2753), i79, i1246, i1278)
2753_0_createMetaList_Store(EOS(STATIC_2753), i79, i1246, i1278) → 2756_0_createMetaList_Load(EOS(STATIC_2756), i79, i1246, i1278)
2756_0_createMetaList_Load(EOS(STATIC_2756), i79, i1246, i1278) → 2761_0_createMetaList_Store(EOS(STATIC_2761), i79, i1246, i1278)
2761_0_createMetaList_Store(EOS(STATIC_2761), i79, i1246, i1278) → 2766_0_createMetaList_Load(EOS(STATIC_2766), i79, i1246, i1278)
2766_0_createMetaList_Load(EOS(STATIC_2766), i79, i1246, i1278) → 2876_0_createMetaList_Load(EOS(STATIC_2876), i79, i1246, i1278)
2876_0_createMetaList_Load(EOS(STATIC_2876), i79, i1246, i1339) → 2879_0_createMetaList_LE(EOS(STATIC_2879), i79, i1246, i1339, i1339)
2879_0_createMetaList_LE(EOS(STATIC_2879), i79, i1246, matching1, matching2) → 2880_0_createMetaList_LE(EOS(STATIC_2880), i79, i1246, 0, 0) | &&(=(matching1, 0), =(matching2, 0))
2879_0_createMetaList_LE(EOS(STATIC_2879), i79, i1246, i1342, i1342) → 2881_0_createMetaList_LE(EOS(STATIC_2881), i79, i1246, i1342, i1342)
2880_0_createMetaList_LE(EOS(STATIC_2880), i79, i1246, matching1, matching2) → 2883_0_createMetaList_New(EOS(STATIC_2883), i79, i1246) | &&(&&(<=(0, 0), =(matching1, 0)), =(matching2, 0))
2883_0_createMetaList_New(EOS(STATIC_2883), i79, i1246) → 2886_0_createMetaList_Duplicate(EOS(STATIC_2886), i79, i1246)
2886_0_createMetaList_Duplicate(EOS(STATIC_2886), i79, i1246) → 2888_0_createMetaList_Load(EOS(STATIC_2888), i79, i1246)
2888_0_createMetaList_Load(EOS(STATIC_2888), i79, i1246) → 2891_0_createMetaList_Load(EOS(STATIC_2891), i79, i1246)
2891_0_createMetaList_Load(EOS(STATIC_2891), i79, i1246) → 2894_0_createMetaList_InvokeMethod(EOS(STATIC_2894), i79, i1246)
2894_0_createMetaList_InvokeMethod(EOS(STATIC_2894), i79, i1246) → 2896_0_<init>_Load(EOS(STATIC_2896), i79, i1246)
2896_0_<init>_Load(EOS(STATIC_2896), i79, i1246) → 2899_0_<init>_InvokeMethod(EOS(STATIC_2899), i79, i1246)
2899_0_<init>_InvokeMethod(EOS(STATIC_2899), i79, i1246) → 2901_0_<init>_Load(EOS(STATIC_2901), i79, i1246)
2901_0_<init>_Load(EOS(STATIC_2901), i79, i1246) → 2903_0_<init>_Load(EOS(STATIC_2903), i79, i1246)
2903_0_<init>_Load(EOS(STATIC_2903), i79, i1246) → 2906_0_<init>_FieldAccess(EOS(STATIC_2906), i79, i1246)
2906_0_<init>_FieldAccess(EOS(STATIC_2906), i79, i1246) → 2910_0_<init>_Load(EOS(STATIC_2910), i79, i1246)
2910_0_<init>_Load(EOS(STATIC_2910), i79, i1246) → 2913_0_<init>_Load(EOS(STATIC_2913), i79, i1246)
2913_0_<init>_Load(EOS(STATIC_2913), i79, i1246) → 2916_0_<init>_FieldAccess(EOS(STATIC_2916), i79, i1246)
2916_0_<init>_FieldAccess(EOS(STATIC_2916), i79, i1246) → 2920_0_<init>_Return(EOS(STATIC_2920), i79, i1246)
2920_0_<init>_Return(EOS(STATIC_2920), i79, i1246) → 2924_0_createMetaList_Store(EOS(STATIC_2924), i79, i1246)
2924_0_createMetaList_Store(EOS(STATIC_2924), i79, i1246) → 2927_0_createMetaList_Inc(EOS(STATIC_2927), i79, i1246)
2927_0_createMetaList_Inc(EOS(STATIC_2927), i79, i1246) → 2930_0_createMetaList_JMP(EOS(STATIC_2930), i79, +(i1246, 1)) | >=(i1246, 0)
2930_0_createMetaList_JMP(EOS(STATIC_2930), i79, i1343) → 2933_0_createMetaList_Load(EOS(STATIC_2933), i79, i1343)
2933_0_createMetaList_Load(EOS(STATIC_2933), i79, i1343) → 2680_0_createMetaList_Load(EOS(STATIC_2680), i79, i1343)
2680_0_createMetaList_Load(EOS(STATIC_2680), i79, i1246) → 2682_0_createMetaList_Load(EOS(STATIC_2682), i79, i1246, i1246)
2881_0_createMetaList_LE(EOS(STATIC_2881), i79, i1246, i1342, i1342) → 2884_0_createMetaList_New(EOS(STATIC_2884), i79, i1246, i1342) | >(i1342, 0)
2884_0_createMetaList_New(EOS(STATIC_2884), i79, i1246, i1342) → 2887_0_createMetaList_Duplicate(EOS(STATIC_2887), i79, i1246, i1342)
2887_0_createMetaList_Duplicate(EOS(STATIC_2887), i79, i1246, i1342) → 2890_0_createMetaList_ConstantStackPush(EOS(STATIC_2890), i79, i1246, i1342)
2890_0_createMetaList_ConstantStackPush(EOS(STATIC_2890), i79, i1246, i1342) → 2892_0_createMetaList_Load(EOS(STATIC_2892), i79, i1246, i1342)
2892_0_createMetaList_Load(EOS(STATIC_2892), i79, i1246, i1342) → 2895_0_createMetaList_InvokeMethod(EOS(STATIC_2895), i79, i1246, i1342)
2895_0_createMetaList_InvokeMethod(EOS(STATIC_2895), i79, i1246, i1342) → 2898_0_<init>_Load(EOS(STATIC_2898), i79, i1246, i1342)
2898_0_<init>_Load(EOS(STATIC_2898), i79, i1246, i1342) → 2900_0_<init>_InvokeMethod(EOS(STATIC_2900), i79, i1246, i1342)
2900_0_<init>_InvokeMethod(EOS(STATIC_2900), i79, i1246, i1342) → 2902_0_<init>_Load(EOS(STATIC_2902), i79, i1246, i1342)
2902_0_<init>_Load(EOS(STATIC_2902), i79, i1246, i1342) → 2905_0_<init>_Load(EOS(STATIC_2905), i79, i1246, i1342)
2905_0_<init>_Load(EOS(STATIC_2905), i79, i1246, i1342) → 2908_0_<init>_FieldAccess(EOS(STATIC_2908), i79, i1246, i1342)
2908_0_<init>_FieldAccess(EOS(STATIC_2908), i79, i1246, i1342) → 2912_0_<init>_Load(EOS(STATIC_2912), i79, i1246, i1342)
2912_0_<init>_Load(EOS(STATIC_2912), i79, i1246, i1342) → 2915_0_<init>_Load(EOS(STATIC_2915), i79, i1246, i1342)
2915_0_<init>_Load(EOS(STATIC_2915), i79, i1246, i1342) → 2918_0_<init>_FieldAccess(EOS(STATIC_2918), i79, i1246, i1342)
2918_0_<init>_FieldAccess(EOS(STATIC_2918), i79, i1246, i1342) → 2923_0_<init>_Return(EOS(STATIC_2923), i79, i1246, i1342)
2923_0_<init>_Return(EOS(STATIC_2923), i79, i1246, i1342) → 2926_0_createMetaList_Store(EOS(STATIC_2926), i79, i1246, i1342)
2926_0_createMetaList_Store(EOS(STATIC_2926), i79, i1246, i1342) → 2928_0_createMetaList_Inc(EOS(STATIC_2928), i79, i1246, i1342)
2928_0_createMetaList_Inc(EOS(STATIC_2928), i79, i1246, i1342) → 2931_0_createMetaList_JMP(EOS(STATIC_2931), i79, i1246, +(i1342, -1)) | >(i1342, 0)
2931_0_createMetaList_JMP(EOS(STATIC_2931), i79, i1246, i1344) → 2935_0_createMetaList_Load(EOS(STATIC_2935), i79, i1246, i1344)
2935_0_createMetaList_Load(EOS(STATIC_2935), i79, i1246, i1344) → 2876_0_createMetaList_Load(EOS(STATIC_2876), i79, i1246, i1344)
R rules:

Combined rules. Obtained 2 conditional rules for P and 0 conditional rules for R.

P rules:
2879_0_createMetaList_LE(EOS(STATIC_2879), x0, x1, 0, 0) → 2879_0_createMetaList_LE(EOS(STATIC_2879), x0, +(x1, 1), x4, x4) | &&(&&(>(+(x4, 1), 0), >(+(x1, 1), 0)), >(x0, +(x1, 1)))
2879_0_createMetaList_LE(EOS(STATIC_2879), x0, x1, x2, x2) → 2879_0_createMetaList_LE(EOS(STATIC_2879), x0, x1, +(x2, -1), +(x2, -1)) | >(x2, 0)
R rules:

Filtered ground terms:

2879_0_createMetaList_LE(x1, x2, x3, x4, x5) → 2879_0_createMetaList_LE(x2, x3, x4, x5)
EOS(x1) → EOS
Cond_2879_0_createMetaList_LE1(x1, x2, x3, x4, x5, x6) → Cond_2879_0_createMetaList_LE1(x1, x3, x4, x5, x6)
Cond_2879_0_createMetaList_LE(x1, x2, x3, x4, x5, x6, x7) → Cond_2879_0_createMetaList_LE(x1, x3, x4, x7)

Filtered duplicate args:

2879_0_createMetaList_LE(x1, x2, x3, x4) → 2879_0_createMetaList_LE(x1, x2, x4)
Cond_2879_0_createMetaList_LE1(x1, x2, x3, x4, x5) → Cond_2879_0_createMetaList_LE1(x1, x2, x3, x5)

Combined rules. Obtained 2 conditional rules for P and 0 conditional rules for R.

P rules:
2879_0_createMetaList_LE(x0, x1, 0) → 2879_0_createMetaList_LE(x0, +(x1, 1), x4) | &&(&&(>(x4, -1), >(x1, -1)), >(x0, +(x1, 1)))
2879_0_createMetaList_LE(x0, x1, x2) → 2879_0_createMetaList_LE(x0, x1, +(x2, -1)) | >(x2, 0)
R rules:

Finished conversion. Obtained 4 rules for P and 0 rules for R. System has predefined symbols.

P rules:
2879_0_CREATEMETALIST_LE(x0, x1, 0) → COND_2879_0_CREATEMETALIST_LE(&&(&&(>(x4, -1), >(x1, -1)), >(x0, +(x1, 1))), x0, x1, 0, x4)
COND_2879_0_CREATEMETALIST_LE(TRUE, x0, x1, 0, x4) → 2879_0_CREATEMETALIST_LE(x0, +(x1, 1), x4)
2879_0_CREATEMETALIST_LE(x0, x1, x2) → COND_2879_0_CREATEMETALIST_LE1(>(x2, 0), x0, x1, x2)
COND_2879_0_CREATEMETALIST_LE1(TRUE, x0, x1, x2) → 2879_0_CREATEMETALIST_LE(x0, x1, +(x2, -1))
R rules:

(22) Obligation:

IDP problem:
The following function symbols are pre-defined:

!=	~	Neq: (Integer, Integer) -> Boolean
*	~	Mul: (Integer, Integer) -> Integer
>=	~	Ge: (Integer, Integer) -> Boolean
-1	~	UnaryMinus: (Integer) -> Integer
\|	~	Bwor: (Integer, Integer) -> Integer
/	~	Div: (Integer, Integer) -> Integer
=	~	Eq: (Integer, Integer) -> Boolean
	~	Bwxor: (Integer, Integer) -> Integer
\|\|	~	Lor: (Boolean, Boolean) -> Boolean
!	~	Lnot: (Boolean) -> Boolean
<	~	Lt: (Integer, Integer) -> Boolean
-	~	Sub: (Integer, Integer) -> Integer
<=	~	Le: (Integer, Integer) -> Boolean
>	~	Gt: (Integer, Integer) -> Boolean
~	~	Bwnot: (Integer) -> Integer
%	~	Mod: (Integer, Integer) -> Integer
&	~	Bwand: (Integer, Integer) -> Integer
+	~	Add: (Integer, Integer) -> Integer
&&	~	Land: (Boolean, Boolean) -> Boolean

The following domains are used:

Boolean, Integer

R is empty.

The integer pair graph contains the following rules and edges:
(0): 2879_0_CREATEMETALIST_LE(x0[0], x1[0], 0) → COND_2879_0_CREATEMETALIST_LE(x4[0] > -1 && x1[0] > -1 && x0[0] > x1[0] + 1, x0[0], x1[0], 0, x4[0])
(1): COND_2879_0_CREATEMETALIST_LE(TRUE, x0[1], x1[1], 0, x4[1]) → 2879_0_CREATEMETALIST_LE(x0[1], x1[1] + 1, x4[1])
(2): 2879_0_CREATEMETALIST_LE(x0[2], x1[2], x2[2]) → COND_2879_0_CREATEMETALIST_LE1(x2[2] > 0, x0[2], x1[2], x2[2])
(3): COND_2879_0_CREATEMETALIST_LE1(TRUE, x0[3], x1[3], x2[3]) → 2879_0_CREATEMETALIST_LE(x0[3], x1[3], x2[3] + -1)

(0) -> (1), if (x4[0] > -1 && x1[0] > -1 && x0[0] > x1[0] + 1 ∧x0[0] →^* x0[1]∧x1[0] →^* x1[1]∧x4[0] →^* x4[1])

(1) -> (0), if (x0[1] →^* x0[0]∧x1[1] + 1 →^* x1[0]∧x4[1] →^* 0)

(1) -> (2), if (x0[1] →^* x0[2]∧x1[1] + 1 →^* x1[2]∧x4[1] →^* x2[2])

(2) -> (3), if (x2[2] > 0 ∧x0[2] →^* x0[3]∧x1[2] →^* x1[3]∧x2[2] →^* x2[3])

(3) -> (0), if (x0[3] →^* x0[0]∧x1[3] →^* x1[0]∧x2[3] + -1 →^* 0)

(3) -> (2), if (x0[3] →^* x0[2]∧x1[3] →^* x1[2]∧x2[3] + -1 →^* x2[2])

The set Q is empty.

(23) IDPNonInfProof (SOUND transformation)

Used the following options for this NonInfProof:
IDPGPoloSolver: Range: [(-1,2)] IsNat: false Interpretation Shape Heuristic: aprove.DPFramework.IDPProblem.Processors.nonInf.poly.IdpDefaultShapeHeuristic@6e2d6f85 Constraint Generator: NonInfConstraintGenerator: PathGenerator: MetricPathGenerator: Max Left Steps: 1 Max Right Steps: 1

The constraints were generated the following way:
The DP Problem is simplified using the Induction Calculus [NONINF] with the following steps:
Note that final constraints are written in bold face.

For Pair 2879_0_CREATEMETALIST_LE(x0, x1, 0) → COND_2879_0_CREATEMETALIST_LE(&&(&&(>(x4, -1), >(x1, -1)), >(x0, +(x1, 1))), x0, x1, 0, x4) the following chains were created:

We consider the chain COND_2879_0_CREATEMETALIST_LE(TRUE, x0[1], x1[1], 0, x4[1]) → 2879_0_CREATEMETALIST_LE(x0[1], +(x1[1], 1), x4[1]), 2879_0_CREATEMETALIST_LE(x0[0], x1[0], 0) → COND_2879_0_CREATEMETALIST_LE(&&(&&(>(x4[0], -1), >(x1[0], -1)), >(x0[0], +(x1[0], 1))), x0[0], x1[0], 0, x4[0]), COND_2879_0_CREATEMETALIST_LE(TRUE, x0[1], x1[1], 0, x4[1]) → 2879_0_CREATEMETALIST_LE(x0[1], +(x1[1], 1), x4[1]) which results in the following constraint:
(1)    (x0[1]=x0[0]∧+(x1[1], 1)=x1[0]∧x4[1]=0∧&&(&&(>(x4[0], -1), >(x1[0], -1)), >(x0[0], +(x1[0], 1)))=TRUE∧x0[0]=x0[1]1∧x1[0]=x1[1]1∧x4[0]=x4[1]1 ⇒ 2879_0_CREATEMETALIST_LE(x0[0], x1[0], 0)≥NonInfC∧2879_0_CREATEMETALIST_LE(x0[0], x1[0], 0)≥COND_2879_0_CREATEMETALIST_LE(&&(&&(>(x4[0], -1), >(x1[0], -1)), >(x0[0], +(x1[0], 1))), x0[0], x1[0], 0, x4[0])∧(U^Increasing(COND_2879_0_CREATEMETALIST_LE(&&(&&(>(x4[0], -1), >(x1[0], -1)), >(x0[0], +(x1[0], 1))), x0[0], x1[0], 0, x4[0])), ≥))

We simplified constraint (1) using rules (III), (IV), (IDP_BOOLEAN) which results in the following new constraint:
(2)    (>(x0[0], +(+(x1[1], 1), 1))=TRUE∧>(x4[0], -1)=TRUE∧>(+(x1[1], 1), -1)=TRUE ⇒ 2879_0_CREATEMETALIST_LE(x0[0], +(x1[1], 1), 0)≥NonInfC∧2879_0_CREATEMETALIST_LE(x0[0], +(x1[1], 1), 0)≥COND_2879_0_CREATEMETALIST_LE(&&(&&(>(x4[0], -1), >(+(x1[1], 1), -1)), >(x0[0], +(+(x1[1], 1), 1))), x0[0], +(x1[1], 1), 0, x4[0])∧(U^Increasing(COND_2879_0_CREATEMETALIST_LE(&&(&&(>(x4[0], -1), >(x1[0], -1)), >(x0[0], +(x1[0], 1))), x0[0], x1[0], 0, x4[0])), ≥))

We simplified constraint (2) using rule (POLY_CONSTRAINTS) which results in the following new constraint:
(3)    (x0[0] + [-3] + [-1]x1[1] ≥ 0∧x4[0] ≥ 0∧x1[1] + [1] ≥ 0 ⇒ (U^Increasing(COND_2879_0_CREATEMETALIST_LE(&&(&&(>(x4[0], -1), >(x1[0], -1)), >(x0[0], +(x1[0], 1))), x0[0], x1[0], 0, x4[0])), ≥)∧[(-2)bni_20 + (-1)Bound*bni_20] + [(-1)bni_20]x1[1] + [bni_20]x0[0] ≥ 0∧[(-1)bso_21] ≥ 0)

We simplified constraint (3) using rule (IDP_POLY_SIMPLIFY) which results in the following new constraint:
(4)    (x0[0] + [-3] + [-1]x1[1] ≥ 0∧x4[0] ≥ 0∧x1[1] + [1] ≥ 0 ⇒ (U^Increasing(COND_2879_0_CREATEMETALIST_LE(&&(&&(>(x4[0], -1), >(x1[0], -1)), >(x0[0], +(x1[0], 1))), x0[0], x1[0], 0, x4[0])), ≥)∧[(-2)bni_20 + (-1)Bound*bni_20] + [(-1)bni_20]x1[1] + [bni_20]x0[0] ≥ 0∧[(-1)bso_21] ≥ 0)

We simplified constraint (4) using rule (POLY_REMOVE_MIN_MAX) which results in the following new constraint:
(5)    (x0[0] + [-3] + [-1]x1[1] ≥ 0∧x4[0] ≥ 0∧x1[1] + [1] ≥ 0 ⇒ (U^Increasing(COND_2879_0_CREATEMETALIST_LE(&&(&&(>(x4[0], -1), >(x1[0], -1)), >(x0[0], +(x1[0], 1))), x0[0], x1[0], 0, x4[0])), ≥)∧[(-2)bni_20 + (-1)Bound*bni_20] + [(-1)bni_20]x1[1] + [bni_20]x0[0] ≥ 0∧[(-1)bso_21] ≥ 0)

We simplified constraint (5) using rule (IDP_SMT_SPLIT) which results in the following new constraint:
(6)    (x0[0] ≥ 0∧x4[0] ≥ 0∧x1[1] + [1] ≥ 0 ⇒ (U^Increasing(COND_2879_0_CREATEMETALIST_LE(&&(&&(>(x4[0], -1), >(x1[0], -1)), >(x0[0], +(x1[0], 1))), x0[0], x1[0], 0, x4[0])), ≥)∧[bni_20 + (-1)Bound*bni_20] + [bni_20]x0[0] ≥ 0∧[(-1)bso_21] ≥ 0)

We simplified constraint (6) using rule (IDP_SMT_SPLIT) which results in the following new constraints:
(7)    (x0[0] ≥ 0∧x4[0] ≥ 0∧[-1]x1[1] + [1] ≥ 0∧x1[1] ≥ 0 ⇒ (U^Increasing(COND_2879_0_CREATEMETALIST_LE(&&(&&(>(x4[0], -1), >(x1[0], -1)), >(x0[0], +(x1[0], 1))), x0[0], x1[0], 0, x4[0])), ≥)∧[bni_20 + (-1)Bound*bni_20] + [bni_20]x0[0] ≥ 0∧[(-1)bso_21] ≥ 0)

(8)    (x0[0] ≥ 0∧x4[0] ≥ 0∧x1[1] + [1] ≥ 0∧x1[1] ≥ 0 ⇒ (U^Increasing(COND_2879_0_CREATEMETALIST_LE(&&(&&(>(x4[0], -1), >(x1[0], -1)), >(x0[0], +(x1[0], 1))), x0[0], x1[0], 0, x4[0])), ≥)∧[bni_20 + (-1)Bound*bni_20] + [bni_20]x0[0] ≥ 0∧[(-1)bso_21] ≥ 0)
We consider the chain COND_2879_0_CREATEMETALIST_LE1(TRUE, x0[3], x1[3], x2[3]) → 2879_0_CREATEMETALIST_LE(x0[3], x1[3], +(x2[3], -1)), 2879_0_CREATEMETALIST_LE(x0[0], x1[0], 0) → COND_2879_0_CREATEMETALIST_LE(&&(&&(>(x4[0], -1), >(x1[0], -1)), >(x0[0], +(x1[0], 1))), x0[0], x1[0], 0, x4[0]), COND_2879_0_CREATEMETALIST_LE(TRUE, x0[1], x1[1], 0, x4[1]) → 2879_0_CREATEMETALIST_LE(x0[1], +(x1[1], 1), x4[1]) which results in the following constraint:
(9)    (x0[3]=x0[0]∧x1[3]=x1[0]∧+(x2[3], -1)=0∧&&(&&(>(x4[0], -1), >(x1[0], -1)), >(x0[0], +(x1[0], 1)))=TRUE∧x0[0]=x0[1]∧x1[0]=x1[1]∧x4[0]=x4[1] ⇒ 2879_0_CREATEMETALIST_LE(x0[0], x1[0], 0)≥NonInfC∧2879_0_CREATEMETALIST_LE(x0[0], x1[0], 0)≥COND_2879_0_CREATEMETALIST_LE(&&(&&(>(x4[0], -1), >(x1[0], -1)), >(x0[0], +(x1[0], 1))), x0[0], x1[0], 0, x4[0])∧(U^Increasing(COND_2879_0_CREATEMETALIST_LE(&&(&&(>(x4[0], -1), >(x1[0], -1)), >(x0[0], +(x1[0], 1))), x0[0], x1[0], 0, x4[0])), ≥))

We simplified constraint (9) using rules (III), (IV), (IDP_BOOLEAN) which results in the following new constraint:
(10)    (+(x2[3], -1)=0∧>(x0[0], +(x1[0], 1))=TRUE∧>(x4[0], -1)=TRUE∧>(x1[0], -1)=TRUE ⇒ 2879_0_CREATEMETALIST_LE(x0[0], x1[0], 0)≥NonInfC∧2879_0_CREATEMETALIST_LE(x0[0], x1[0], 0)≥COND_2879_0_CREATEMETALIST_LE(&&(&&(>(x4[0], -1), >(x1[0], -1)), >(x0[0], +(x1[0], 1))), x0[0], x1[0], 0, x4[0])∧(U^Increasing(COND_2879_0_CREATEMETALIST_LE(&&(&&(>(x4[0], -1), >(x1[0], -1)), >(x0[0], +(x1[0], 1))), x0[0], x1[0], 0, x4[0])), ≥))

We simplified constraint (10) using rule (POLY_CONSTRAINTS) which results in the following new constraint:
(11)    (x2[3] + [-1] ≥ 0∧x0[0] + [-2] + [-1]x1[0] ≥ 0∧x4[0] ≥ 0∧x1[0] ≥ 0 ⇒ (U^Increasing(COND_2879_0_CREATEMETALIST_LE(&&(&&(>(x4[0], -1), >(x1[0], -1)), >(x0[0], +(x1[0], 1))), x0[0], x1[0], 0, x4[0])), ≥)∧[(-1)bni_20 + (-1)Bound*bni_20] + [(-1)bni_20]x1[0] + [bni_20]x0[0] ≥ 0∧[(-1)bso_21] ≥ 0)

We simplified constraint (11) using rule (IDP_POLY_SIMPLIFY) which results in the following new constraint:
(12)    (x2[3] + [-1] ≥ 0∧x0[0] + [-2] + [-1]x1[0] ≥ 0∧x4[0] ≥ 0∧x1[0] ≥ 0 ⇒ (U^Increasing(COND_2879_0_CREATEMETALIST_LE(&&(&&(>(x4[0], -1), >(x1[0], -1)), >(x0[0], +(x1[0], 1))), x0[0], x1[0], 0, x4[0])), ≥)∧[(-1)bni_20 + (-1)Bound*bni_20] + [(-1)bni_20]x1[0] + [bni_20]x0[0] ≥ 0∧[(-1)bso_21] ≥ 0)

We simplified constraint (12) using rule (POLY_REMOVE_MIN_MAX) which results in the following new constraint:
(13)    (x2[3] + [-1] ≥ 0∧x0[0] + [-2] + [-1]x1[0] ≥ 0∧x4[0] ≥ 0∧x1[0] ≥ 0 ⇒ (U^Increasing(COND_2879_0_CREATEMETALIST_LE(&&(&&(>(x4[0], -1), >(x1[0], -1)), >(x0[0], +(x1[0], 1))), x0[0], x1[0], 0, x4[0])), ≥)∧[(-1)bni_20 + (-1)Bound*bni_20] + [(-1)bni_20]x1[0] + [bni_20]x0[0] ≥ 0∧[(-1)bso_21] ≥ 0)

We simplified constraint (13) using rule (IDP_SMT_SPLIT) which results in the following new constraint:
(14)    (x2[3] + [-1] ≥ 0∧x0[0] ≥ 0∧x4[0] ≥ 0∧x1[0] ≥ 0 ⇒ (U^Increasing(COND_2879_0_CREATEMETALIST_LE(&&(&&(>(x4[0], -1), >(x1[0], -1)), >(x0[0], +(x1[0], 1))), x0[0], x1[0], 0, x4[0])), ≥)∧[bni_20 + (-1)Bound*bni_20] + [bni_20]x0[0] ≥ 0∧[(-1)bso_21] ≥ 0)

For Pair COND_2879_0_CREATEMETALIST_LE(TRUE, x0, x1, 0, x4) → 2879_0_CREATEMETALIST_LE(x0, +(x1, 1), x4) the following chains were created:

We consider the chain 2879_0_CREATEMETALIST_LE(x0[0], x1[0], 0) → COND_2879_0_CREATEMETALIST_LE(&&(&&(>(x4[0], -1), >(x1[0], -1)), >(x0[0], +(x1[0], 1))), x0[0], x1[0], 0, x4[0]), COND_2879_0_CREATEMETALIST_LE(TRUE, x0[1], x1[1], 0, x4[1]) → 2879_0_CREATEMETALIST_LE(x0[1], +(x1[1], 1), x4[1]), 2879_0_CREATEMETALIST_LE(x0[0], x1[0], 0) → COND_2879_0_CREATEMETALIST_LE(&&(&&(>(x4[0], -1), >(x1[0], -1)), >(x0[0], +(x1[0], 1))), x0[0], x1[0], 0, x4[0]) which results in the following constraint:
(15)    (&&(&&(>(x4[0], -1), >(x1[0], -1)), >(x0[0], +(x1[0], 1)))=TRUE∧x0[0]=x0[1]∧x1[0]=x1[1]∧x4[0]=x4[1]∧x0[1]=x0[0]1∧+(x1[1], 1)=x1[0]1∧x4[1]=0 ⇒ COND_2879_0_CREATEMETALIST_LE(TRUE, x0[1], x1[1], 0, x4[1])≥NonInfC∧COND_2879_0_CREATEMETALIST_LE(TRUE, x0[1], x1[1], 0, x4[1])≥2879_0_CREATEMETALIST_LE(x0[1], +(x1[1], 1), x4[1])∧(U^Increasing(2879_0_CREATEMETALIST_LE(x0[1], +(x1[1], 1), x4[1])), ≥))

We simplified constraint (15) using rules (III), (IV), (IDP_CONSTANT_FOLD), (DELETE_TRIVIAL_REDUCESTO), (IDP_BOOLEAN) which results in the following new constraint:
(16)    (>(x0[0], +(x1[0], 1))=TRUE∧>(x1[0], -1)=TRUE ⇒ COND_2879_0_CREATEMETALIST_LE(TRUE, x0[0], x1[0], 0, 0)≥NonInfC∧COND_2879_0_CREATEMETALIST_LE(TRUE, x0[0], x1[0], 0, 0)≥2879_0_CREATEMETALIST_LE(x0[0], +(x1[0], 1), 0)∧(U^Increasing(2879_0_CREATEMETALIST_LE(x0[1], +(x1[1], 1), x4[1])), ≥))

We simplified constraint (16) using rule (POLY_CONSTRAINTS) which results in the following new constraint:
(17)    (x0[0] + [-2] + [-1]x1[0] ≥ 0∧x1[0] ≥ 0 ⇒ (U^Increasing(2879_0_CREATEMETALIST_LE(x0[1], +(x1[1], 1), x4[1])), ≥)∧[(-1)bni_22 + (-1)Bound*bni_22] + [(-1)bni_22]x1[0] + [bni_22]x0[0] ≥ 0∧[1 + (-1)bso_23] ≥ 0)

We simplified constraint (17) using rule (IDP_POLY_SIMPLIFY) which results in the following new constraint:
(18)    (x0[0] + [-2] + [-1]x1[0] ≥ 0∧x1[0] ≥ 0 ⇒ (U^Increasing(2879_0_CREATEMETALIST_LE(x0[1], +(x1[1], 1), x4[1])), ≥)∧[(-1)bni_22 + (-1)Bound*bni_22] + [(-1)bni_22]x1[0] + [bni_22]x0[0] ≥ 0∧[1 + (-1)bso_23] ≥ 0)

We simplified constraint (18) using rule (POLY_REMOVE_MIN_MAX) which results in the following new constraint:
(19)    (x0[0] + [-2] + [-1]x1[0] ≥ 0∧x1[0] ≥ 0 ⇒ (U^Increasing(2879_0_CREATEMETALIST_LE(x0[1], +(x1[1], 1), x4[1])), ≥)∧[(-1)bni_22 + (-1)Bound*bni_22] + [(-1)bni_22]x1[0] + [bni_22]x0[0] ≥ 0∧[1 + (-1)bso_23] ≥ 0)

We simplified constraint (19) using rule (IDP_SMT_SPLIT) which results in the following new constraint:
(20)    (x0[0] ≥ 0∧x1[0] ≥ 0 ⇒ (U^Increasing(2879_0_CREATEMETALIST_LE(x0[1], +(x1[1], 1), x4[1])), ≥)∧[bni_22 + (-1)Bound*bni_22] + [bni_22]x0[0] ≥ 0∧[1 + (-1)bso_23] ≥ 0)
We consider the chain 2879_0_CREATEMETALIST_LE(x0[0], x1[0], 0) → COND_2879_0_CREATEMETALIST_LE(&&(&&(>(x4[0], -1), >(x1[0], -1)), >(x0[0], +(x1[0], 1))), x0[0], x1[0], 0, x4[0]), COND_2879_0_CREATEMETALIST_LE(TRUE, x0[1], x1[1], 0, x4[1]) → 2879_0_CREATEMETALIST_LE(x0[1], +(x1[1], 1), x4[1]), 2879_0_CREATEMETALIST_LE(x0[2], x1[2], x2[2]) → COND_2879_0_CREATEMETALIST_LE1(>(x2[2], 0), x0[2], x1[2], x2[2]) which results in the following constraint:
(21)    (&&(&&(>(x4[0], -1), >(x1[0], -1)), >(x0[0], +(x1[0], 1)))=TRUE∧x0[0]=x0[1]∧x1[0]=x1[1]∧x4[0]=x4[1]∧x0[1]=x0[2]∧+(x1[1], 1)=x1[2]∧x4[1]=x2[2] ⇒ COND_2879_0_CREATEMETALIST_LE(TRUE, x0[1], x1[1], 0, x4[1])≥NonInfC∧COND_2879_0_CREATEMETALIST_LE(TRUE, x0[1], x1[1], 0, x4[1])≥2879_0_CREATEMETALIST_LE(x0[1], +(x1[1], 1), x4[1])∧(U^Increasing(2879_0_CREATEMETALIST_LE(x0[1], +(x1[1], 1), x4[1])), ≥))

We simplified constraint (21) using rules (III), (IV), (IDP_BOOLEAN) which results in the following new constraint:
(22)    (>(x0[0], +(x1[0], 1))=TRUE∧>(x4[0], -1)=TRUE∧>(x1[0], -1)=TRUE ⇒ COND_2879_0_CREATEMETALIST_LE(TRUE, x0[0], x1[0], 0, x4[0])≥NonInfC∧COND_2879_0_CREATEMETALIST_LE(TRUE, x0[0], x1[0], 0, x4[0])≥2879_0_CREATEMETALIST_LE(x0[0], +(x1[0], 1), x4[0])∧(U^Increasing(2879_0_CREATEMETALIST_LE(x0[1], +(x1[1], 1), x4[1])), ≥))

We simplified constraint (22) using rule (POLY_CONSTRAINTS) which results in the following new constraint:
(23)    (x0[0] + [-2] + [-1]x1[0] ≥ 0∧x4[0] ≥ 0∧x1[0] ≥ 0 ⇒ (U^Increasing(2879_0_CREATEMETALIST_LE(x0[1], +(x1[1], 1), x4[1])), ≥)∧[(-1)bni_22 + (-1)Bound*bni_22] + [(-1)bni_22]x1[0] + [bni_22]x0[0] ≥ 0∧[1 + (-1)bso_23] ≥ 0)

We simplified constraint (23) using rule (IDP_POLY_SIMPLIFY) which results in the following new constraint:
(24)    (x0[0] + [-2] + [-1]x1[0] ≥ 0∧x4[0] ≥ 0∧x1[0] ≥ 0 ⇒ (U^Increasing(2879_0_CREATEMETALIST_LE(x0[1], +(x1[1], 1), x4[1])), ≥)∧[(-1)bni_22 + (-1)Bound*bni_22] + [(-1)bni_22]x1[0] + [bni_22]x0[0] ≥ 0∧[1 + (-1)bso_23] ≥ 0)

We simplified constraint (24) using rule (POLY_REMOVE_MIN_MAX) which results in the following new constraint:
(25)    (x0[0] + [-2] + [-1]x1[0] ≥ 0∧x4[0] ≥ 0∧x1[0] ≥ 0 ⇒ (U^Increasing(2879_0_CREATEMETALIST_LE(x0[1], +(x1[1], 1), x4[1])), ≥)∧[(-1)bni_22 + (-1)Bound*bni_22] + [(-1)bni_22]x1[0] + [bni_22]x0[0] ≥ 0∧[1 + (-1)bso_23] ≥ 0)

We simplified constraint (25) using rule (IDP_SMT_SPLIT) which results in the following new constraint:
(26)    (x0[0] ≥ 0∧x4[0] ≥ 0∧x1[0] ≥ 0 ⇒ (U^Increasing(2879_0_CREATEMETALIST_LE(x0[1], +(x1[1], 1), x4[1])), ≥)∧[bni_22 + (-1)Bound*bni_22] + [bni_22]x0[0] ≥ 0∧[1 + (-1)bso_23] ≥ 0)

For Pair 2879_0_CREATEMETALIST_LE(x0, x1, x2) → COND_2879_0_CREATEMETALIST_LE1(>(x2, 0), x0, x1, x2) the following chains were created:

We consider the chain 2879_0_CREATEMETALIST_LE(x0[2], x1[2], x2[2]) → COND_2879_0_CREATEMETALIST_LE1(>(x2[2], 0), x0[2], x1[2], x2[2]), COND_2879_0_CREATEMETALIST_LE1(TRUE, x0[3], x1[3], x2[3]) → 2879_0_CREATEMETALIST_LE(x0[3], x1[3], +(x2[3], -1)) which results in the following constraint:
(27)    (>(x2[2], 0)=TRUE∧x0[2]=x0[3]∧x1[2]=x1[3]∧x2[2]=x2[3] ⇒ 2879_0_CREATEMETALIST_LE(x0[2], x1[2], x2[2])≥NonInfC∧2879_0_CREATEMETALIST_LE(x0[2], x1[2], x2[2])≥COND_2879_0_CREATEMETALIST_LE1(>(x2[2], 0), x0[2], x1[2], x2[2])∧(U^Increasing(COND_2879_0_CREATEMETALIST_LE1(>(x2[2], 0), x0[2], x1[2], x2[2])), ≥))

We simplified constraint (27) using rule (IV) which results in the following new constraint:
(28)    (>(x2[2], 0)=TRUE ⇒ 2879_0_CREATEMETALIST_LE(x0[2], x1[2], x2[2])≥NonInfC∧2879_0_CREATEMETALIST_LE(x0[2], x1[2], x2[2])≥COND_2879_0_CREATEMETALIST_LE1(>(x2[2], 0), x0[2], x1[2], x2[2])∧(U^Increasing(COND_2879_0_CREATEMETALIST_LE1(>(x2[2], 0), x0[2], x1[2], x2[2])), ≥))

We simplified constraint (28) using rule (POLY_CONSTRAINTS) which results in the following new constraint:
(29)    (x2[2] + [-1] ≥ 0 ⇒ (U^Increasing(COND_2879_0_CREATEMETALIST_LE1(>(x2[2], 0), x0[2], x1[2], x2[2])), ≥)∧[(-1)bni_24 + (-1)Bound*bni_24] + [(-1)bni_24]x1[2] + [bni_24]x0[2] ≥ 0∧[(-1)bso_25] ≥ 0)

We simplified constraint (29) using rule (IDP_POLY_SIMPLIFY) which results in the following new constraint:
(30)    (x2[2] + [-1] ≥ 0 ⇒ (U^Increasing(COND_2879_0_CREATEMETALIST_LE1(>(x2[2], 0), x0[2], x1[2], x2[2])), ≥)∧[(-1)bni_24 + (-1)Bound*bni_24] + [(-1)bni_24]x1[2] + [bni_24]x0[2] ≥ 0∧[(-1)bso_25] ≥ 0)

We simplified constraint (30) using rule (POLY_REMOVE_MIN_MAX) which results in the following new constraint:
(31)    (x2[2] + [-1] ≥ 0 ⇒ (U^Increasing(COND_2879_0_CREATEMETALIST_LE1(>(x2[2], 0), x0[2], x1[2], x2[2])), ≥)∧[(-1)bni_24 + (-1)Bound*bni_24] + [(-1)bni_24]x1[2] + [bni_24]x0[2] ≥ 0∧[(-1)bso_25] ≥ 0)

We simplified constraint (31) using rule (IDP_UNRESTRICTED_VARS) which results in the following new constraint:
(32)    (x2[2] + [-1] ≥ 0 ⇒ (U^Increasing(COND_2879_0_CREATEMETALIST_LE1(>(x2[2], 0), x0[2], x1[2], x2[2])), ≥)∧[(-1)bni_24] = 0∧[bni_24] = 0∧[(-1)bni_24 + (-1)Bound*bni_24] ≥ 0∧0 = 0∧0 = 0∧[(-1)bso_25] ≥ 0)

We simplified constraint (32) using rule (IDP_SMT_SPLIT) which results in the following new constraint:
(33)    (x2[2] ≥ 0 ⇒ (U^Increasing(COND_2879_0_CREATEMETALIST_LE1(>(x2[2], 0), x0[2], x1[2], x2[2])), ≥)∧[(-1)bni_24] = 0∧[bni_24] = 0∧[(-1)bni_24 + (-1)Bound*bni_24] ≥ 0∧0 = 0∧0 = 0∧[(-1)bso_25] ≥ 0)

For Pair COND_2879_0_CREATEMETALIST_LE1(TRUE, x0, x1, x2) → 2879_0_CREATEMETALIST_LE(x0, x1, +(x2, -1)) the following chains were created:

We consider the chain 2879_0_CREATEMETALIST_LE(x0[2], x1[2], x2[2]) → COND_2879_0_CREATEMETALIST_LE1(>(x2[2], 0), x0[2], x1[2], x2[2]), COND_2879_0_CREATEMETALIST_LE1(TRUE, x0[3], x1[3], x2[3]) → 2879_0_CREATEMETALIST_LE(x0[3], x1[3], +(x2[3], -1)), 2879_0_CREATEMETALIST_LE(x0[0], x1[0], 0) → COND_2879_0_CREATEMETALIST_LE(&&(&&(>(x4[0], -1), >(x1[0], -1)), >(x0[0], +(x1[0], 1))), x0[0], x1[0], 0, x4[0]) which results in the following constraint:
(34)    (>(x2[2], 0)=TRUE∧x0[2]=x0[3]∧x1[2]=x1[3]∧x2[2]=x2[3]∧x0[3]=x0[0]∧x1[3]=x1[0]∧+(x2[3], -1)=0 ⇒ COND_2879_0_CREATEMETALIST_LE1(TRUE, x0[3], x1[3], x2[3])≥NonInfC∧COND_2879_0_CREATEMETALIST_LE1(TRUE, x0[3], x1[3], x2[3])≥2879_0_CREATEMETALIST_LE(x0[3], x1[3], +(x2[3], -1))∧(U^Increasing(2879_0_CREATEMETALIST_LE(x0[3], x1[3], +(x2[3], -1))), ≥))

We simplified constraint (34) using rules (III), (IV) which results in the following new constraint:
(35)    (>(x2[2], 0)=TRUE∧+(x2[2], -1)=0 ⇒ COND_2879_0_CREATEMETALIST_LE1(TRUE, x0[2], x1[2], x2[2])≥NonInfC∧COND_2879_0_CREATEMETALIST_LE1(TRUE, x0[2], x1[2], x2[2])≥2879_0_CREATEMETALIST_LE(x0[2], x1[2], +(x2[2], -1))∧(U^Increasing(2879_0_CREATEMETALIST_LE(x0[3], x1[3], +(x2[3], -1))), ≥))

We simplified constraint (35) using rule (POLY_CONSTRAINTS) which results in the following new constraint:
(36)    (x2[2] + [-1] ≥ 0∧x2[2] + [-1] ≥ 0 ⇒ (U^Increasing(2879_0_CREATEMETALIST_LE(x0[3], x1[3], +(x2[3], -1))), ≥)∧[(-1)bni_26 + (-1)Bound*bni_26] + [(-1)bni_26]x1[2] + [bni_26]x0[2] ≥ 0∧[(-1)bso_27] ≥ 0)

We simplified constraint (36) using rule (IDP_POLY_SIMPLIFY) which results in the following new constraint:
(37)    (x2[2] + [-1] ≥ 0∧x2[2] + [-1] ≥ 0 ⇒ (U^Increasing(2879_0_CREATEMETALIST_LE(x0[3], x1[3], +(x2[3], -1))), ≥)∧[(-1)bni_26 + (-1)Bound*bni_26] + [(-1)bni_26]x1[2] + [bni_26]x0[2] ≥ 0∧[(-1)bso_27] ≥ 0)

We simplified constraint (37) using rule (POLY_REMOVE_MIN_MAX) which results in the following new constraint:
(38)    (x2[2] + [-1] ≥ 0∧x2[2] + [-1] ≥ 0 ⇒ (U^Increasing(2879_0_CREATEMETALIST_LE(x0[3], x1[3], +(x2[3], -1))), ≥)∧[(-1)bni_26 + (-1)Bound*bni_26] + [(-1)bni_26]x1[2] + [bni_26]x0[2] ≥ 0∧[(-1)bso_27] ≥ 0)

We simplified constraint (38) using rule (IDP_UNRESTRICTED_VARS) which results in the following new constraint:
(39)    (x2[2] + [-1] ≥ 0∧x2[2] + [-1] ≥ 0 ⇒ (U^Increasing(2879_0_CREATEMETALIST_LE(x0[3], x1[3], +(x2[3], -1))), ≥)∧[(-1)bni_26] = 0∧[bni_26] = 0∧[(-1)bni_26 + (-1)Bound*bni_26] ≥ 0∧0 = 0∧0 = 0∧[(-1)bso_27] ≥ 0)

We simplified constraint (39) using rule (IDP_SMT_SPLIT) which results in the following new constraint:
(40)    (x2[2] ≥ 0∧x2[2] ≥ 0 ⇒ (U^Increasing(2879_0_CREATEMETALIST_LE(x0[3], x1[3], +(x2[3], -1))), ≥)∧[(-1)bni_26] = 0∧[bni_26] = 0∧[(-1)bni_26 + (-1)Bound*bni_26] ≥ 0∧0 = 0∧0 = 0∧[(-1)bso_27] ≥ 0)
We consider the chain 2879_0_CREATEMETALIST_LE(x0[2], x1[2], x2[2]) → COND_2879_0_CREATEMETALIST_LE1(>(x2[2], 0), x0[2], x1[2], x2[2]), COND_2879_0_CREATEMETALIST_LE1(TRUE, x0[3], x1[3], x2[3]) → 2879_0_CREATEMETALIST_LE(x0[3], x1[3], +(x2[3], -1)), 2879_0_CREATEMETALIST_LE(x0[2], x1[2], x2[2]) → COND_2879_0_CREATEMETALIST_LE1(>(x2[2], 0), x0[2], x1[2], x2[2]) which results in the following constraint:
(41)    (>(x2[2], 0)=TRUE∧x0[2]=x0[3]∧x1[2]=x1[3]∧x2[2]=x2[3]∧x0[3]=x0[2]1∧x1[3]=x1[2]1∧+(x2[3], -1)=x2[2]1 ⇒ COND_2879_0_CREATEMETALIST_LE1(TRUE, x0[3], x1[3], x2[3])≥NonInfC∧COND_2879_0_CREATEMETALIST_LE1(TRUE, x0[3], x1[3], x2[3])≥2879_0_CREATEMETALIST_LE(x0[3], x1[3], +(x2[3], -1))∧(U^Increasing(2879_0_CREATEMETALIST_LE(x0[3], x1[3], +(x2[3], -1))), ≥))

We simplified constraint (41) using rules (III), (IV) which results in the following new constraint:
(42)    (>(x2[2], 0)=TRUE ⇒ COND_2879_0_CREATEMETALIST_LE1(TRUE, x0[2], x1[2], x2[2])≥NonInfC∧COND_2879_0_CREATEMETALIST_LE1(TRUE, x0[2], x1[2], x2[2])≥2879_0_CREATEMETALIST_LE(x0[2], x1[2], +(x2[2], -1))∧(U^Increasing(2879_0_CREATEMETALIST_LE(x0[3], x1[3], +(x2[3], -1))), ≥))

We simplified constraint (42) using rule (POLY_CONSTRAINTS) which results in the following new constraint:
(43)    (x2[2] + [-1] ≥ 0 ⇒ (U^Increasing(2879_0_CREATEMETALIST_LE(x0[3], x1[3], +(x2[3], -1))), ≥)∧[(-1)bni_26 + (-1)Bound*bni_26] + [(-1)bni_26]x1[2] + [bni_26]x0[2] ≥ 0∧[(-1)bso_27] ≥ 0)

We simplified constraint (43) using rule (IDP_POLY_SIMPLIFY) which results in the following new constraint:
(44)    (x2[2] + [-1] ≥ 0 ⇒ (U^Increasing(2879_0_CREATEMETALIST_LE(x0[3], x1[3], +(x2[3], -1))), ≥)∧[(-1)bni_26 + (-1)Bound*bni_26] + [(-1)bni_26]x1[2] + [bni_26]x0[2] ≥ 0∧[(-1)bso_27] ≥ 0)

We simplified constraint (44) using rule (POLY_REMOVE_MIN_MAX) which results in the following new constraint:
(45)    (x2[2] + [-1] ≥ 0 ⇒ (U^Increasing(2879_0_CREATEMETALIST_LE(x0[3], x1[3], +(x2[3], -1))), ≥)∧[(-1)bni_26 + (-1)Bound*bni_26] + [(-1)bni_26]x1[2] + [bni_26]x0[2] ≥ 0∧[(-1)bso_27] ≥ 0)

We simplified constraint (45) using rule (IDP_UNRESTRICTED_VARS) which results in the following new constraint:
(46)    (x2[2] + [-1] ≥ 0 ⇒ (U^Increasing(2879_0_CREATEMETALIST_LE(x0[3], x1[3], +(x2[3], -1))), ≥)∧[(-1)bni_26] = 0∧[bni_26] = 0∧[(-1)bni_26 + (-1)Bound*bni_26] ≥ 0∧0 = 0∧0 = 0∧[(-1)bso_27] ≥ 0)

We simplified constraint (46) using rule (IDP_SMT_SPLIT) which results in the following new constraint:
(47)    (x2[2] ≥ 0 ⇒ (U^Increasing(2879_0_CREATEMETALIST_LE(x0[3], x1[3], +(x2[3], -1))), ≥)∧[(-1)bni_26] = 0∧[bni_26] = 0∧[(-1)bni_26 + (-1)Bound*bni_26] ≥ 0∧0 = 0∧0 = 0∧[(-1)bso_27] ≥ 0)

To summarize, we get the following constraints P_≥ for the following pairs.

2879_0_CREATEMETALIST_LE(x0, x1, 0) → COND_2879_0_CREATEMETALIST_LE(&&(&&(>(x4, -1), >(x1, -1)), >(x0, +(x1, 1))), x0, x1, 0, x4)
- (x0[0] ≥ 0∧x4[0] ≥ 0∧[-1]x1[1] + [1] ≥ 0∧x1[1] ≥ 0 ⇒ (U^Increasing(COND_2879_0_CREATEMETALIST_LE(&&(&&(>(x4[0], -1), >(x1[0], -1)), >(x0[0], +(x1[0], 1))), x0[0], x1[0], 0, x4[0])), ≥)∧[bni_20 + (-1)Bound*bni_20] + [bni_20]x0[0] ≥ 0∧[(-1)bso_21] ≥ 0)
- (x0[0] ≥ 0∧x4[0] ≥ 0∧x1[1] + [1] ≥ 0∧x1[1] ≥ 0 ⇒ (U^Increasing(COND_2879_0_CREATEMETALIST_LE(&&(&&(>(x4[0], -1), >(x1[0], -1)), >(x0[0], +(x1[0], 1))), x0[0], x1[0], 0, x4[0])), ≥)∧[bni_20 + (-1)Bound*bni_20] + [bni_20]x0[0] ≥ 0∧[(-1)bso_21] ≥ 0)
- (x2[3] + [-1] ≥ 0∧x0[0] ≥ 0∧x4[0] ≥ 0∧x1[0] ≥ 0 ⇒ (U^Increasing(COND_2879_0_CREATEMETALIST_LE(&&(&&(>(x4[0], -1), >(x1[0], -1)), >(x0[0], +(x1[0], 1))), x0[0], x1[0], 0, x4[0])), ≥)∧[bni_20 + (-1)Bound*bni_20] + [bni_20]x0[0] ≥ 0∧[(-1)bso_21] ≥ 0)
COND_2879_0_CREATEMETALIST_LE(TRUE, x0, x1, 0, x4) → 2879_0_CREATEMETALIST_LE(x0, +(x1, 1), x4)
- (x0[0] ≥ 0∧x1[0] ≥ 0 ⇒ (U^Increasing(2879_0_CREATEMETALIST_LE(x0[1], +(x1[1], 1), x4[1])), ≥)∧[bni_22 + (-1)Bound*bni_22] + [bni_22]x0[0] ≥ 0∧[1 + (-1)bso_23] ≥ 0)
- (x0[0] ≥ 0∧x4[0] ≥ 0∧x1[0] ≥ 0 ⇒ (U^Increasing(2879_0_CREATEMETALIST_LE(x0[1], +(x1[1], 1), x4[1])), ≥)∧[bni_22 + (-1)Bound*bni_22] + [bni_22]x0[0] ≥ 0∧[1 + (-1)bso_23] ≥ 0)
2879_0_CREATEMETALIST_LE(x0, x1, x2) → COND_2879_0_CREATEMETALIST_LE1(>(x2, 0), x0, x1, x2)
- (x2[2] ≥ 0 ⇒ (U^Increasing(COND_2879_0_CREATEMETALIST_LE1(>(x2[2], 0), x0[2], x1[2], x2[2])), ≥)∧[(-1)bni_24] = 0∧[bni_24] = 0∧[(-1)bni_24 + (-1)Bound*bni_24] ≥ 0∧0 = 0∧0 = 0∧[(-1)bso_25] ≥ 0)
COND_2879_0_CREATEMETALIST_LE1(TRUE, x0, x1, x2) → 2879_0_CREATEMETALIST_LE(x0, x1, +(x2, -1))
- (x2[2] ≥ 0∧x2[2] ≥ 0 ⇒ (U^Increasing(2879_0_CREATEMETALIST_LE(x0[3], x1[3], +(x2[3], -1))), ≥)∧[(-1)bni_26] = 0∧[bni_26] = 0∧[(-1)bni_26 + (-1)Bound*bni_26] ≥ 0∧0 = 0∧0 = 0∧[(-1)bso_27] ≥ 0)
- (x2[2] ≥ 0 ⇒ (U^Increasing(2879_0_CREATEMETALIST_LE(x0[3], x1[3], +(x2[3], -1))), ≥)∧[(-1)bni_26] = 0∧[bni_26] = 0∧[(-1)bni_26 + (-1)Bound*bni_26] ≥ 0∧0 = 0∧0 = 0∧[(-1)bso_27] ≥ 0)

The constraints for P_> respective P_bound are constructed from P_≥ where we just replace every occurence of "t ≥ s" in P_≥ by "t > s" respective "t ≥ c". Here c stands for the fresh constant used for P_bound.
Using the following integer polynomial ordering the resulting constraints can be solved
Polynomial interpretation over integers[POLO]:

POL(TRUE) = 0
POL(FALSE) = 0
POL(2879_0_CREATEMETALIST_LE(x₁, x₂, x₃)) = [-1] + [-1]x₂ + x₁
POL(0) = 0
POL(COND_2879_0_CREATEMETALIST_LE(x₁, x₂, x₃, x₄, x₅)) = [-1] + [-1]x₄ + [-1]x₃ + x₂
POL(&&(x₁, x₂)) = [-1]
POL(>(x₁, x₂)) = [-1]
POL(-1) = [-1]
POL(+(x₁, x₂)) = x₁ + x₂
POL(1) = [1]
POL(COND_2879_0_CREATEMETALIST_LE1(x₁, x₂, x₃, x₄)) = [-1] + [-1]x₃ + x₂

The following pairs are in P_>:

COND_2879_0_CREATEMETALIST_LE(TRUE, x0[1], x1[1], 0, x4[1]) → 2879_0_CREATEMETALIST_LE(x0[1], +(x1[1], 1), x4[1])

The following pairs are in P_bound:

2879_0_CREATEMETALIST_LE(x0[0], x1[0], 0) → COND_2879_0_CREATEMETALIST_LE(&&(&&(>(x4[0], -1), >(x1[0], -1)), >(x0[0], +(x1[0], 1))), x0[0], x1[0], 0, x4[0])
COND_2879_0_CREATEMETALIST_LE(TRUE, x0[1], x1[1], 0, x4[1]) → 2879_0_CREATEMETALIST_LE(x0[1], +(x1[1], 1), x4[1])

The following pairs are in P_≥:

2879_0_CREATEMETALIST_LE(x0[0], x1[0], 0) → COND_2879_0_CREATEMETALIST_LE(&&(&&(>(x4[0], -1), >(x1[0], -1)), >(x0[0], +(x1[0], 1))), x0[0], x1[0], 0, x4[0])
2879_0_CREATEMETALIST_LE(x0[2], x1[2], x2[2]) → COND_2879_0_CREATEMETALIST_LE1(>(x2[2], 0), x0[2], x1[2], x2[2])
COND_2879_0_CREATEMETALIST_LE1(TRUE, x0[3], x1[3], x2[3]) → 2879_0_CREATEMETALIST_LE(x0[3], x1[3], +(x2[3], -1))

At least the following rules have been oriented under context sensitive arithmetic replacement:

TRUE¹ → &&(TRUE, TRUE)¹
FALSE¹ → &&(TRUE, FALSE)¹
FALSE¹ → &&(FALSE, TRUE)¹
FALSE¹ → &&(FALSE, FALSE)¹

(24) Obligation:

IDP problem:
The following function symbols are pre-defined:

!=	~	Neq: (Integer, Integer) -> Boolean
*	~	Mul: (Integer, Integer) -> Integer
>=	~	Ge: (Integer, Integer) -> Boolean
-1	~	UnaryMinus: (Integer) -> Integer
\|	~	Bwor: (Integer, Integer) -> Integer
/	~	Div: (Integer, Integer) -> Integer
=	~	Eq: (Integer, Integer) -> Boolean
	~	Bwxor: (Integer, Integer) -> Integer
\|\|	~	Lor: (Boolean, Boolean) -> Boolean
!	~	Lnot: (Boolean) -> Boolean
<	~	Lt: (Integer, Integer) -> Boolean
-	~	Sub: (Integer, Integer) -> Integer
<=	~	Le: (Integer, Integer) -> Boolean
>	~	Gt: (Integer, Integer) -> Boolean
~	~	Bwnot: (Integer) -> Integer
%	~	Mod: (Integer, Integer) -> Integer
&	~	Bwand: (Integer, Integer) -> Integer
+	~	Add: (Integer, Integer) -> Integer
&&	~	Land: (Boolean, Boolean) -> Boolean

The following domains are used:

Boolean, Integer

R is empty.

The integer pair graph contains the following rules and edges:
(0): 2879_0_CREATEMETALIST_LE(x0[0], x1[0], 0) → COND_2879_0_CREATEMETALIST_LE(x4[0] > -1 && x1[0] > -1 && x0[0] > x1[0] + 1, x0[0], x1[0], 0, x4[0])
(2): 2879_0_CREATEMETALIST_LE(x0[2], x1[2], x2[2]) → COND_2879_0_CREATEMETALIST_LE1(x2[2] > 0, x0[2], x1[2], x2[2])
(3): COND_2879_0_CREATEMETALIST_LE1(TRUE, x0[3], x1[3], x2[3]) → 2879_0_CREATEMETALIST_LE(x0[3], x1[3], x2[3] + -1)

(3) -> (0), if (x0[3] →^* x0[0]∧x1[3] →^* x1[0]∧x2[3] + -1 →^* 0)

(3) -> (2), if (x0[3] →^* x0[2]∧x1[3] →^* x1[2]∧x2[3] + -1 →^* x2[2])

(2) -> (3), if (x2[2] > 0 ∧x0[2] →^* x0[3]∧x1[2] →^* x1[3]∧x2[2] →^* x2[3])

The set Q is empty.

(25) IDependencyGraphProof (EQUIVALENT transformation)

The approximation of the Dependency Graph [LPAR04,FROCOS05,EDGSTAR] contains 1 SCC with 1 less node.

(26) Obligation:

IDP problem:
The following function symbols are pre-defined:

!=	~	Neq: (Integer, Integer) -> Boolean
*	~	Mul: (Integer, Integer) -> Integer
>=	~	Ge: (Integer, Integer) -> Boolean
-1	~	UnaryMinus: (Integer) -> Integer
\|	~	Bwor: (Integer, Integer) -> Integer
/	~	Div: (Integer, Integer) -> Integer
=	~	Eq: (Integer, Integer) -> Boolean
	~	Bwxor: (Integer, Integer) -> Integer
\|\|	~	Lor: (Boolean, Boolean) -> Boolean
!	~	Lnot: (Boolean) -> Boolean
<	~	Lt: (Integer, Integer) -> Boolean
-	~	Sub: (Integer, Integer) -> Integer
<=	~	Le: (Integer, Integer) -> Boolean
>	~	Gt: (Integer, Integer) -> Boolean
~	~	Bwnot: (Integer) -> Integer
%	~	Mod: (Integer, Integer) -> Integer
&	~	Bwand: (Integer, Integer) -> Integer
+	~	Add: (Integer, Integer) -> Integer
&&	~	Land: (Boolean, Boolean) -> Boolean

The following domains are used:

Integer

R is empty.

The integer pair graph contains the following rules and edges:
(3): COND_2879_0_CREATEMETALIST_LE1(TRUE, x0[3], x1[3], x2[3]) → 2879_0_CREATEMETALIST_LE(x0[3], x1[3], x2[3] + -1)
(2): 2879_0_CREATEMETALIST_LE(x0[2], x1[2], x2[2]) → COND_2879_0_CREATEMETALIST_LE1(x2[2] > 0, x0[2], x1[2], x2[2])

(3) -> (2), if (x0[3] →^* x0[2]∧x1[3] →^* x1[2]∧x2[3] + -1 →^* x2[2])

(2) -> (3), if (x2[2] > 0 ∧x0[2] →^* x0[3]∧x1[2] →^* x1[3]∧x2[2] →^* x2[3])

The set Q is empty.

(27) IDPNonInfProof (SOUND transformation)

Used the following options for this NonInfProof:
IDPGPoloSolver: Range: [(-1,2)] IsNat: false Interpretation Shape Heuristic: aprove.DPFramework.IDPProblem.Processors.nonInf.poly.IdpDefaultShapeHeuristic@6e2d6f85 Constraint Generator: NonInfConstraintGenerator: PathGenerator: MetricPathGenerator: Max Left Steps: 1 Max Right Steps: 1

The constraints were generated the following way:
The DP Problem is simplified using the Induction Calculus [NONINF] with the following steps:
Note that final constraints are written in bold face.

For Pair COND_2879_0_CREATEMETALIST_LE1(TRUE, x0[3], x1[3], x2[3]) → 2879_0_CREATEMETALIST_LE(x0[3], x1[3], +(x2[3], -1)) the following chains were created:

We consider the chain 2879_0_CREATEMETALIST_LE(x0[2], x1[2], x2[2]) → COND_2879_0_CREATEMETALIST_LE1(>(x2[2], 0), x0[2], x1[2], x2[2]), COND_2879_0_CREATEMETALIST_LE1(TRUE, x0[3], x1[3], x2[3]) → 2879_0_CREATEMETALIST_LE(x0[3], x1[3], +(x2[3], -1)), 2879_0_CREATEMETALIST_LE(x0[2], x1[2], x2[2]) → COND_2879_0_CREATEMETALIST_LE1(>(x2[2], 0), x0[2], x1[2], x2[2]) which results in the following constraint:
(1)    (>(x2[2], 0)=TRUE∧x0[2]=x0[3]∧x1[2]=x1[3]∧x2[2]=x2[3]∧x0[3]=x0[2]1∧x1[3]=x1[2]1∧+(x2[3], -1)=x2[2]1 ⇒ COND_2879_0_CREATEMETALIST_LE1(TRUE, x0[3], x1[3], x2[3])≥NonInfC∧COND_2879_0_CREATEMETALIST_LE1(TRUE, x0[3], x1[3], x2[3])≥2879_0_CREATEMETALIST_LE(x0[3], x1[3], +(x2[3], -1))∧(U^Increasing(2879_0_CREATEMETALIST_LE(x0[3], x1[3], +(x2[3], -1))), ≥))

We simplified constraint (1) using rules (III), (IV) which results in the following new constraint:
(2)    (>(x2[2], 0)=TRUE ⇒ COND_2879_0_CREATEMETALIST_LE1(TRUE, x0[2], x1[2], x2[2])≥NonInfC∧COND_2879_0_CREATEMETALIST_LE1(TRUE, x0[2], x1[2], x2[2])≥2879_0_CREATEMETALIST_LE(x0[2], x1[2], +(x2[2], -1))∧(U^Increasing(2879_0_CREATEMETALIST_LE(x0[3], x1[3], +(x2[3], -1))), ≥))

We simplified constraint (2) using rule (POLY_CONSTRAINTS) which results in the following new constraint:
(3)    (x2[2] + [-1] ≥ 0 ⇒ (U^Increasing(2879_0_CREATEMETALIST_LE(x0[3], x1[3], +(x2[3], -1))), ≥)∧[(-1)bni_13 + (-1)Bound*bni_13] + [bni_13]x2[2] ≥ 0∧[1 + (-1)bso_14] ≥ 0)

We simplified constraint (3) using rule (IDP_POLY_SIMPLIFY) which results in the following new constraint:
(4)    (x2[2] + [-1] ≥ 0 ⇒ (U^Increasing(2879_0_CREATEMETALIST_LE(x0[3], x1[3], +(x2[3], -1))), ≥)∧[(-1)bni_13 + (-1)Bound*bni_13] + [bni_13]x2[2] ≥ 0∧[1 + (-1)bso_14] ≥ 0)

We simplified constraint (4) using rule (POLY_REMOVE_MIN_MAX) which results in the following new constraint:
(5)    (x2[2] + [-1] ≥ 0 ⇒ (U^Increasing(2879_0_CREATEMETALIST_LE(x0[3], x1[3], +(x2[3], -1))), ≥)∧[(-1)bni_13 + (-1)Bound*bni_13] + [bni_13]x2[2] ≥ 0∧[1 + (-1)bso_14] ≥ 0)

We simplified constraint (5) using rule (IDP_UNRESTRICTED_VARS) which results in the following new constraint:
(6)    (x2[2] + [-1] ≥ 0 ⇒ (U^Increasing(2879_0_CREATEMETALIST_LE(x0[3], x1[3], +(x2[3], -1))), ≥)∧0 = 0∧0 = 0∧[(-1)bni_13 + (-1)Bound*bni_13] + [bni_13]x2[2] ≥ 0∧0 = 0∧0 = 0∧[1 + (-1)bso_14] ≥ 0)

We simplified constraint (6) using rule (IDP_SMT_SPLIT) which results in the following new constraint:
(7)    (x2[2] ≥ 0 ⇒ (U^Increasing(2879_0_CREATEMETALIST_LE(x0[3], x1[3], +(x2[3], -1))), ≥)∧0 = 0∧0 = 0∧[(-1)Bound*bni_13] + [bni_13]x2[2] ≥ 0∧0 = 0∧0 = 0∧[1 + (-1)bso_14] ≥ 0)

For Pair 2879_0_CREATEMETALIST_LE(x0[2], x1[2], x2[2]) → COND_2879_0_CREATEMETALIST_LE1(>(x2[2], 0), x0[2], x1[2], x2[2]) the following chains were created:

We consider the chain 2879_0_CREATEMETALIST_LE(x0[2], x1[2], x2[2]) → COND_2879_0_CREATEMETALIST_LE1(>(x2[2], 0), x0[2], x1[2], x2[2]), COND_2879_0_CREATEMETALIST_LE1(TRUE, x0[3], x1[3], x2[3]) → 2879_0_CREATEMETALIST_LE(x0[3], x1[3], +(x2[3], -1)) which results in the following constraint:
(8)    (>(x2[2], 0)=TRUE∧x0[2]=x0[3]∧x1[2]=x1[3]∧x2[2]=x2[3] ⇒ 2879_0_CREATEMETALIST_LE(x0[2], x1[2], x2[2])≥NonInfC∧2879_0_CREATEMETALIST_LE(x0[2], x1[2], x2[2])≥COND_2879_0_CREATEMETALIST_LE1(>(x2[2], 0), x0[2], x1[2], x2[2])∧(U^Increasing(COND_2879_0_CREATEMETALIST_LE1(>(x2[2], 0), x0[2], x1[2], x2[2])), ≥))

We simplified constraint (8) using rule (IV) which results in the following new constraint:
(9)    (>(x2[2], 0)=TRUE ⇒ 2879_0_CREATEMETALIST_LE(x0[2], x1[2], x2[2])≥NonInfC∧2879_0_CREATEMETALIST_LE(x0[2], x1[2], x2[2])≥COND_2879_0_CREATEMETALIST_LE1(>(x2[2], 0), x0[2], x1[2], x2[2])∧(U^Increasing(COND_2879_0_CREATEMETALIST_LE1(>(x2[2], 0), x0[2], x1[2], x2[2])), ≥))

We simplified constraint (9) using rule (POLY_CONSTRAINTS) which results in the following new constraint:
(10)    (x2[2] + [-1] ≥ 0 ⇒ (U^Increasing(COND_2879_0_CREATEMETALIST_LE1(>(x2[2], 0), x0[2], x1[2], x2[2])), ≥)∧[(-1)bni_15 + (-1)Bound*bni_15] + [bni_15]x2[2] ≥ 0∧[(-1)bso_16] ≥ 0)

We simplified constraint (10) using rule (IDP_POLY_SIMPLIFY) which results in the following new constraint:
(11)    (x2[2] + [-1] ≥ 0 ⇒ (U^Increasing(COND_2879_0_CREATEMETALIST_LE1(>(x2[2], 0), x0[2], x1[2], x2[2])), ≥)∧[(-1)bni_15 + (-1)Bound*bni_15] + [bni_15]x2[2] ≥ 0∧[(-1)bso_16] ≥ 0)

We simplified constraint (11) using rule (POLY_REMOVE_MIN_MAX) which results in the following new constraint:
(12)    (x2[2] + [-1] ≥ 0 ⇒ (U^Increasing(COND_2879_0_CREATEMETALIST_LE1(>(x2[2], 0), x0[2], x1[2], x2[2])), ≥)∧[(-1)bni_15 + (-1)Bound*bni_15] + [bni_15]x2[2] ≥ 0∧[(-1)bso_16] ≥ 0)

We simplified constraint (12) using rule (IDP_UNRESTRICTED_VARS) which results in the following new constraint:
(13)    (x2[2] + [-1] ≥ 0 ⇒ (U^Increasing(COND_2879_0_CREATEMETALIST_LE1(>(x2[2], 0), x0[2], x1[2], x2[2])), ≥)∧0 = 0∧0 = 0∧[(-1)bni_15 + (-1)Bound*bni_15] + [bni_15]x2[2] ≥ 0∧0 = 0∧0 = 0∧[(-1)bso_16] ≥ 0)

We simplified constraint (13) using rule (IDP_SMT_SPLIT) which results in the following new constraint:
(14)    (x2[2] ≥ 0 ⇒ (U^Increasing(COND_2879_0_CREATEMETALIST_LE1(>(x2[2], 0), x0[2], x1[2], x2[2])), ≥)∧0 = 0∧0 = 0∧[(-1)Bound*bni_15] + [bni_15]x2[2] ≥ 0∧0 = 0∧0 = 0∧[(-1)bso_16] ≥ 0)

To summarize, we get the following constraints P_≥ for the following pairs.

COND_2879_0_CREATEMETALIST_LE1(TRUE, x0[3], x1[3], x2[3]) → 2879_0_CREATEMETALIST_LE(x0[3], x1[3], +(x2[3], -1))
- (x2[2] ≥ 0 ⇒ (U^Increasing(2879_0_CREATEMETALIST_LE(x0[3], x1[3], +(x2[3], -1))), ≥)∧0 = 0∧0 = 0∧[(-1)Bound*bni_13] + [bni_13]x2[2] ≥ 0∧0 = 0∧0 = 0∧[1 + (-1)bso_14] ≥ 0)
2879_0_CREATEMETALIST_LE(x0[2], x1[2], x2[2]) → COND_2879_0_CREATEMETALIST_LE1(>(x2[2], 0), x0[2], x1[2], x2[2])
- (x2[2] ≥ 0 ⇒ (U^Increasing(COND_2879_0_CREATEMETALIST_LE1(>(x2[2], 0), x0[2], x1[2], x2[2])), ≥)∧0 = 0∧0 = 0∧[(-1)Bound*bni_15] + [bni_15]x2[2] ≥ 0∧0 = 0∧0 = 0∧[(-1)bso_16] ≥ 0)

POL(TRUE) = 0
POL(FALSE) = 0
POL(COND_2879_0_CREATEMETALIST_LE1(x₁, x₂, x₃, x₄)) = [-1] + x₄
POL(2879_0_CREATEMETALIST_LE(x₁, x₂, x₃)) = [-1] + x₃
POL(+(x₁, x₂)) = x₁ + x₂
POL(-1) = [-1]
POL(>(x₁, x₂)) = [-1]
POL(0) = 0

The following pairs are in P_>:

COND_2879_0_CREATEMETALIST_LE1(TRUE, x0[3], x1[3], x2[3]) → 2879_0_CREATEMETALIST_LE(x0[3], x1[3], +(x2[3], -1))

The following pairs are in P_bound:

COND_2879_0_CREATEMETALIST_LE1(TRUE, x0[3], x1[3], x2[3]) → 2879_0_CREATEMETALIST_LE(x0[3], x1[3], +(x2[3], -1))
2879_0_CREATEMETALIST_LE(x0[2], x1[2], x2[2]) → COND_2879_0_CREATEMETALIST_LE1(>(x2[2], 0), x0[2], x1[2], x2[2])

The following pairs are in P_≥:

2879_0_CREATEMETALIST_LE(x0[2], x1[2], x2[2]) → COND_2879_0_CREATEMETALIST_LE1(>(x2[2], 0), x0[2], x1[2], x2[2])

There are no usable rules.

(28) Obligation:

IDP problem:
The following function symbols are pre-defined:

!=	~	Neq: (Integer, Integer) -> Boolean
*	~	Mul: (Integer, Integer) -> Integer
>=	~	Ge: (Integer, Integer) -> Boolean
-1	~	UnaryMinus: (Integer) -> Integer
\|	~	Bwor: (Integer, Integer) -> Integer
/	~	Div: (Integer, Integer) -> Integer
=	~	Eq: (Integer, Integer) -> Boolean
	~	Bwxor: (Integer, Integer) -> Integer
\|\|	~	Lor: (Boolean, Boolean) -> Boolean
!	~	Lnot: (Boolean) -> Boolean
<	~	Lt: (Integer, Integer) -> Boolean
-	~	Sub: (Integer, Integer) -> Integer
<=	~	Le: (Integer, Integer) -> Boolean
>	~	Gt: (Integer, Integer) -> Boolean
~	~	Bwnot: (Integer) -> Integer
%	~	Mod: (Integer, Integer) -> Integer
&	~	Bwand: (Integer, Integer) -> Integer
+	~	Add: (Integer, Integer) -> Integer
&&	~	Land: (Boolean, Boolean) -> Boolean

The following domains are used:

Integer

R is empty.

The integer pair graph contains the following rules and edges:
(2): 2879_0_CREATEMETALIST_LE(x0[2], x1[2], x2[2]) → COND_2879_0_CREATEMETALIST_LE1(x2[2] > 0, x0[2], x1[2], x2[2])

The set Q is empty.

(29) IDependencyGraphProof (EQUIVALENT transformation)

The approximation of the Dependency Graph [LPAR04,FROCOS05,EDGSTAR] contains 0 SCCs with 1 less node.

(0) Obligation:

(1) JBCToGraph (SOUND transformation)

(2) Obligation:

(3) TerminationGraphToSCCProof (SOUND transformation)

(4) Complex Obligation (AND)

(5) Obligation:

(6) SCCToIDPv1Proof (SOUND transformation)

(7) Obligation:

(8) IDPtoQDPProof (SOUND transformation)

(9) Obligation:

(10) UsableRulesProof (EQUIVALENT transformation)

(11) Obligation:

(12) QReductionProof (EQUIVALENT transformation)

(13) Obligation:

(14) UsableRulesReductionPairsProof (EQUIVALENT transformation)

(15) Obligation:

(16) MRRProof (EQUIVALENT transformation)

(17) Obligation:

(18) PisEmptyProof (EQUIVALENT transformation)

(19) YES

(20) Obligation:

(21) SCCToIDPv1Proof (SOUND transformation)

(22) Obligation:

(23) IDPNonInfProof (SOUND transformation)

(24) Obligation:

(25) IDependencyGraphProof (EQUIVALENT transformation)

(26) Obligation:

(27) IDPNonInfProof (SOUND transformation)

(28) Obligation:

(29) IDependencyGraphProof (EQUIVALENT transformation)

(30) TRUE